I’m trying to write “info.rkt” for my project. Is there a way to list all its dependencies? Or, at least, to tell me if I’m missing any?

@leafac raco setup --check-pkg-deps

see all --fix-pkg-deps

note that running it on just your collection will do the right thing but it’s possible for it to miss dependencies

Thank you :slightly_smiling_face:

hi!

hi

@lexi.lambda coming back to your questions:

1. yes, bidirectional checking and local argument synthesis are different things and can be separated. for example, you could just drop polymorphism entirely, and use bidirectionality to infer the type annotations on lambdas in some cases

1. variable elimination is necessary so that you don’t end up with constraints referring to variables that aren’t in scope

and yes, it’s necessary even without subtyping

the key to understanding variable elimination is in the CG-Fun rule, where we prevent the generated constraints from referring to the bound variables in the individual function types

this is necessary because those variables don’t make sense to use outside of their scope

1. the way constraint generation works is that it generates some constraints on variables that make S <: T

so that if we pick a substitution for those variables that meets those constraints, and apply that substitution to both S and T, producing S’ and T’, then S’ <: T’

the judgment V \|-_X S <: T => C says that we generate constraints C to make S <: T in that way

the Xs are the variables we want to know about

and the Vs are variables that should not be mentioned in the constraints

hope that helps

@samth: That does help. I will probably try and work through a simple example on pen and paper when I have some time to try and better understand how it all works.

what’s the place for documentation bug reports (the guide, in this case)? the main racket repo at github?

@andreiformiga that’s the right place

jerryj: I’m catching up rather late, but I wrote some blog post tutorials for the FFI a while back. Perhaps the blog format would be less overwhelming. Anyhow, any feedback appreciated and hope it helps. http://prl.ccs.neu.edu/blog/2016/06/27/tutorial-using-racket-s-ffi/

Hi asumu, thanks for reaching out to me. Actually, I happened to find part 1 of your tutorial, it was very helpful. I didn’t notice you had a part 2 and part 3, so i’ll check those out after I finish reading the “Inside: Racket C API” doc. I get the sense that I’ll need to know all those kinds of black magic to truley become self-sufficient in the ffi realm.

I realized sending a PR for a fix would be as much work as submitting an issue, but I’m not sure how to fix it.

https://github.com/racket/racket/issues/1661

@samth: Looking over the paper again, I am still a little perplexed by what the constraint generation section is actually describing. It would appear that the various constraint generation rules only inspect types, not terms. Which type are these rules actually applied to? If the type of the argument is known, how is that incorporated into this process? Perhaps I’m overlooking something obvious, but some of the notation seems sort of opaque to me.

I’m trying to apply this to a very simple example. Given an environment with const : All(X, Y) X → Y → X and an expression const True "hello", where True can be inferred to have type Bool and "hello" can be inferred to have type String, I’m trying to understand how this process produces X <: Bool and Y <: String.

@lexi.lambda so, the key rule is App-Inf-Alg

in the terms of that rule, f is All(X,Y) X, Y -> X (I’m using multiple arg functions because the paper does), and the es are True and "hello" and thus the Ss are Bool and String

the Xs are X,Y

so then we make two calls to the constraint generation algorithm:

1. \empty \|-_{X,Y} Bool <: X => C1

1. \empty \|-_{X,Y} String <: Y => C2

that produces two constraints: Bool <: X <: Top and String <: Y <: Top

then we have to take the conjunction of those two constraints, and determine a minimal substitution for R

here R is just X, and so the minimal substitution is X \|-> Bool (minimal in the sense that it produces the least type in the subtyping order)

then we apply that substitution to R, which gives Bool, and that the type of the whole application

@samth: Aha, I see; I think I overlooked App-InfAlg. That all makes sense, though, thank you. I’ll probably have more questions later, but I’ll try and work through some other examples on my own.