In this context, how can something be a “type” and a “function from types to values” at the same time?

oh, you said “the type of a function from types to values” so I’m not actually sure how to phrase the question that would help me, lol

@rokitna What are you having trouble with?

I should be a little less short. There are two good approaches to polymorphic types and type constructors. One is what you see in a language with dependent types, like Idris. There, the List type constructor is a function that takes a type and produces a type; it’s type is Type -> Type. Similarly, a “polymorphic function” is just one whose first argument is a type. So map takes a type, and then another type, and then a function, and then a list.

The other approach is what you see in Haskell or Java or Rust. There, type constructors are like in Idris, but functions can have a polymorphic type. So the first argument of map is a function, and the map value is classified by a quantified type.

The second approach goes naturally with type inference, where an instantiation of the type is chosen automatically. In contrast, in the first approach type inference doesn’t make much sense. Instead, in languages like that you have implicit arguments, where the type checker tries to supply some arguments for you.

Sometimes those arguments are called implicit arguments, which means they are almost always automatically deduced.

Thanks for all that detail. I think I put together a few of the pieces myself right after my messages, but I wasn’t sure it was all the pieces. I didn’t want to flail too much with endless follow-up messages. :stuck_out_tongue:

This response did fill in a couple more gaps for me. I think where I originally got confused was this: If we’re talking about types, there are the constructors of the types and the constructors of their values.

At first I understood @kellysmith12.21 to be saying that it’s a mistake for there to be a type constructor that constructs a forall type. Then how would you write down a forall type at all? (But I can make some sense of this if I try: Perhaps “type constructor” can be a certain subset of type formers, and the forall type former doesn’t count as a type constructor for some reason.)

With the gaps filled in, now I think I understand that the mistake @kellysmith12.21 was talking about was to expect there to be a type constructor that constructed the values of a forall type. In general, the inhabitants of a type are constructed by value constructors. (In the specific case where the forall type is forall a. Type, then it makes sense to construct inhabitants of that type using a type constructor.)

Unless I’m mistaken, I think what @samth described is a different scenario, where the choice is between letting inhabitants of type b be treated simultaneously as inhabitants of type forall a. b or requiring the inhabitants of type forall a. b to have a wrapper around them.

I get the impression @kellysmith12.21 is really trying to refer to the same scenario. So perhaps in this context, “type constructor” really is referring to a certain subset of type formers, namely those which form types whose inhabitants have dedicated value constructors. Am I on the right track? In this case, I think I’m still confused about something, which is what the actual mistake is that’s being discussed here. What goes wrong when the inhabitants of forall a. b are represented differently than inhabitants of b? (I think I might have heard about challenges that arose in Typed Racket before, but I guess I don’t remember.)

I didn’t get to the part of where Typed Racket did something wrong. What Typed Racket does (that is bad) is conflate polymorphic types (ie, terms of that have the type Type -> T for some plain old type T) with type constructors (terms of type Type -> Type)

And then it tries to do inference when you use map, which has a forall type, but also the type of map can be a type constructor, where you don’t do inference.

The type of map can be a type constructor? I’m a little lost there… (It’s probably something I’ve heard of and that I’d remember if I tried to use the language a bit…)

The type of map is (All (A B) (-> (-> A B) (Listof A) (Listof B))) (roughly). You can just write (define-type maptype <that>) and then write the type (maptype Integer String).

Oh, that looks familiar to me indeed, and now what @kellysmith12.21 originally said makes a whole new kind of sense to me. I think I’m finally on the same page. Thank you! :)

You can??? That’s wild.

> (define-type maptype (All (A B) (-> (-> A B) (Listof A) (Listof B)))) > (:type (maptype Integer String)) (-> (-> Integer String) (Listof Integer) (Listof String)) [can expand further: Integer] > (ann map (maptype Integer String)) - : (-> (-> Integer String) (Listof Integer) (Listof String))

wow O.o

yeah that’s. nontraditional, to say the least.

Bad is the word I’d use

What flavor of type inference does Typed Racket use?