@maxsnew re: your tweet: which one of those is explicit in Typed Racket?

casts are explicit in TR because they are specified at module boundaries

but my understanding is that TR has unusual parametricity enforcement

so it might not apply directly

I’m currently working on something where sealing is explicit and therefore accessible to the programmer even in dynamically typed code

but I don’t think my solution works without making polymorphism explicit as well :confused:

@maxsnew casts don’t need to be explicit if you can synthesize them during type checking

for example, they aren’t explicit for typed->untyped casts

our DLS paper has no explicit casts

you just need a simple type system

a module boundary is an explicit cast

I don’t understand — there’s a simple type-directed translation from the GTLC to the system in my DLS paper

so? there’s a simple type-directed translation from GTLC into explicit cast calculi also

also isn’t polymorphism explicit in TR (as in you have to annotate to get a polymorphic type, not that you explicitly instantiate)

w.r.t. polymorphism in TR, a polymorphic type is only used when explicitly annotated as such. More generally, unannotated arguments are given type Any generally speaking.

right versus trying to generalize like in https://link.springer.com/chapter/10.1007/978-3-319-89884-1_1

… I don’t immediately understand the comparison (and have not read that paper, to be clear). They say “the first goal of this paper is to propose a generalization of consistent subtyping that is adequate for polymorphic subtyping”… Typed Racket does not use consistent subtyping at all, or consistency while performing inference, because both of these things are done in an entirely statically typed context, which makes me think this isn’t the right comparison and/or isn’t addressing the overarching question/comment you have about TR

sorry you’re missing some context from a tweet that Sam TH was referencing don’t worry about it

@maxsnew right, generalization is explicit in TR (but that’s not necessary for the gradual typing part) but instantiation (what you said in the tweet) is implicit

yes though instantiation in typed code doesn’t seal anything so it’s not really what I was talking about

right but the important case, which is instantiation of functions casted to a polymorphic type, is also implicit

ok well I’m sure my tweet was wrong/too pithy

Hello Everyone! Hope all are well! I have a quick questions for Racket 6.6 with the language Scheme, what packages do I need to have with it?

I have the simply scheme by danny yoo which is used with the simply scheme curriculum, but things like (first ’truffle) is throwing an error: first: contract violation expected: (and/c list? (not/c empty?))

@jlshown what did you expect the expression (first 'truffle) to do? (i.e. I don’t understand the problem, because that error seems appropriate and accurate to me)

@maxsnew the reason that I bring it up is that I think all of those features are required for a sensible account of gradual polymorphism

in the sense that you don’t write any of them explicitly in an untyped language, so requiring them breaks some fundamental part of the approach

@jlshown (ah sorry, I glanced over at the simply scheme text and see it’s supposed to return ’t)

but you do make sealing explicit in a dynamic language, the difference between a value and a value wrapped in an opaque struct is not implicit at all

@jlshown try installing https://pkgs.racket-lang.org/package/simply-scheme

I disagree; map doesn’t do any sealing in Racket

people use sealing in dynamic languages to represent existentials, usually

@jlshown In DrRacket (v6.6) I clicked File > Package Manager, then entered simply-scheme in the text box and clicked install, and the following program now works: #lang simply-scheme (first 'truffle)

i.e. producing 't

I agree map doesn’t seal

it is also not parametric

what do you mean? the standard definition is certainly parameteric

sorry didn’t think that through

map is parametric, there’s no difference whether it is sealed or not

I’m not saying that sealing is implicitly used in dynamic languages to enforce parametricity

I’m saying that the language feature that corresponds to sealing (generative structs, units) is not implicit in the dynamically typed language

the language design I have works for existential types, making it work for forall types is a bit strange I admit

i agree with that about existentials

but I think universals have to be implicit

I sort of agree but only inasmuch as I think sealing for universals is not really what anybody wants

well dynamic enforcement of gradual types isn’t something anyone “wants” in a certain sense

I think people do like opaque structs?

I certainly do

and so conclude that people do want dynamic enforcement of existentials

I feel like the question of “want” is problematic

ok

@pnwamk Thank you so much, what I will do is uninstall the package or racket if I have to then, reinstall racket + simply-scheme and try it again. I will let you know.

@pnwamk yes (first ’truffle ) would be ’t