I'm basically trying to do the equivalent of this simple `fold` function: --- module Simple = struct type term = | Int of int | Add | App of term * term let rec fold i f = function | Int _ as t -> f i t | Add -> f i Add | App (x, y) as t -> f (fold (fold i f x) f y) t end --- ... but using a GADT: --- module Gadt = struct type _ term = | Int : int -> int term | Add : (int -> int -> int) term | App : ('b -> 'a) term * 'b term -> 'a term let rec fold : type a. 'r -> ('r -> _ term -> 'r) -> 'r = fun i f -> function | Int _ as t -> f i t | Add -> f i Add (* ^ Error: This pattern matches values of type (int -> int -> int) term but a pattern was expected which matches values of type int term Type int -> int -> int is not compatible with type int *) | App (x, y) as t -> f (fold (fold i f x) f y) t end --- I've tried other variants of the syntax and got many encouragements but no green flag from the type-checker. Why is the compiler expecting an int term in there? I though the whole point of the `type a. ...` syntax was to allow the matched type to vary from one pattern to the next? Is there a way to do this?

[-- Attachment #1: Type: text/plain, Size: 2097 bytes --] On Tue, Jan 7, 2020 at 2:25 PM <rixed@happyleptic.org> wrote: > ... but using a GADT: > > --- > module Gadt = > struct > type _ term = > | Int : int -> int term > | Add : (int -> int -> int) term > | App : ('b -> 'a) term * 'b term -> 'a term > > let rec fold : type a. 'r -> ('r -> _ term -> 'r) -> 'r = fun i f -> > function > | Int _ as t -> f i t > | Add -> f i Add > (* > ^ Error: This pattern matches values of type (int -> int -> int) term > but a pattern was expected which matches values of type int term > Type int -> int -> int is not compatible with type int > *) > | App (x, y) as t -> f (fold (fold i f x) f y) t > end > --- > > I've tried other variants of the syntax and got many encouragements but no > green flag from the type-checker. > Why is the compiler expecting an int term in there? I though the whole > point of the `type a. ...` syntax was to allow the matched type to vary > from one pattern to the next? > Is there a way to do this? > It is the limitation of the let-bound polymorphism. A parameter of a function is monomorphic in its body. The classical example doesn't even reference any GADT, let example f = f "hello", f 42 It won't compile even though we can provide a polymorphic function that can applied both to integers and to strings, e.g., `exampe (fun x -> x)` should be possible, but not, because of the let-bounded polymorphism. There are a few solutions available in OCaml, the simplest is to use records, e.g., type app = {apply : 'a. 'a -> 'a} let example {apply} = apply "hello", apply 42;; val example : app -> string * int = <fun> Now we have `app` that is polymorphic. In your case, I would define a visitor type, e.g., type 'r visitor = {visit : 'a. 'a term -> 'r -> 'r} let rec fold : type a. 'r -> 'r visitor -> a term -> 'r = fun i f t -> match t with | Int _ as t -> f.visit i t | Add as t -> f.visit i t | App (x,y) as t -> let i = fold i f x in let i = fold i f y in f.visit i t Cheers, Ivan Gotovchits [-- Attachment #2: Type: text/html, Size: 3077 bytes --] <div dir="ltr"><div dir="ltr"><br></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Jan 7, 2020 at 2:25 PM <<a href="mailto:rixed@happyleptic.org">rixed@happyleptic.org</a>> wrote:</div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"> ... but using a GADT:<br> <br> ---<br> module Gadt =<br> struct<br> type _ term =<br> | Int : int -> int term<br> | Add : (int -> int -> int) term<br> | App : ('b -> 'a) term * 'b term -> 'a term<br> <br> let rec fold : type a. 'r -> ('r -> _ term -> 'r) -> 'r = fun i f -> function<br> | Int _ as t -> f i t<br> | Add -> f i Add<br> (*<br> ^ Error: This pattern matches values of type (int -> int -> int) term<br> but a pattern was expected which matches values of type int term<br> Type int -> int -> int is not compatible with type int<br> *)<br> | App (x, y) as t -> f (fold (fold i f x) f y) t<br> end<br> ---<br> <br> I've tried other variants of the syntax and got many encouragements but no green flag from the type-checker.<br> Why is the compiler expecting an int term in there? I though the whole point of the `type a. ...` syntax was to allow the matched type to vary from one pattern to the next?<br> Is there a way to do this?<br></blockquote><div> </div><div>It is the limitation of the let-bound polymorphism. A parameter of a function is monomorphic in its body. The classical example doesn't even reference any GADT,</div><div><br></div><div> let example f = f "hello", f 42</div><div><br></div><div>It won't compile even though we can provide a polymorphic function that can applied both to integers and to strings, e.g., `exampe (fun x -> x)` should be possible, but not, because of the let-bounded polymorphism. There are a few solutions available in OCaml, the simplest is to use records, e.g.,</div><div><br></div><div> type app = {apply : 'a. 'a -> 'a}<br><br></div><div> let example {apply} = apply "hello", apply 42;; <br> val example : app -> string * int = <fun><br></div><div> </div><div>Now we have `app` that is polymorphic. </div><div>In your case, I would define a visitor type, e.g.,</div><div><br></div><div> type 'r visitor = {visit : 'a. 'a term -> 'r -> 'r}</div><div><br></div><div> let rec fold : type a. 'r -> 'r visitor -> a term -> 'r =<br> fun i f t -> match t with<br> | Int _ as t -> f.visit i t<br> | Add as t -> f.visit i t<br> | App (x,y) as t -><br> let i = fold i f x in<br> let i = fold i f y in<br> f.visit i t</div><div><br></div><div><br></div><div>Cheers,</div><div>Ivan Gotovchits</div><div> </div><div><br></div></div></div>

```
Hello and thank you for the answer.
On Tue, Jan 7, 2020, at 21:21, Ivan Gotovchits wrote:
> It is the limitation of the let-bound polymorphism. (...)
> In your case, I would define a visitor type, e.g.,
> type 'r visitor = {visit : 'a. 'a term -> 'r -> 'r}
Oh I see. I've used this trick to force a function to be polymorphic, but I failed to see that this was the problem because to me `f` is not any more polymorphic when the `term` is a GADT than when it's not.
So there is no lighter syntax to specify that `f` should accept any member of a GADT than the syntax to specify that `f` should accept any type at all?
I wonder, is this just a limitation of the OCaml parser or is there some deep reason for these work-around (like is the case, from my understanding, for the value restriction)?
Sorry for asking such simple questions but I've build a mental model of how OCaml type checking works mostly from trials and errors, which used to work great until some versions ago :)
```

```
Actually, this is a rare case where using a polymorphic method may be
handy too:
let rec fold : type a r. r -> <v : 'b. r -> 'b term -> r> -> a term -> r =
fun i f -> function
| Int _ as t -> f#v i t
| Add -> f#v i Add
| App (x, y) as t -> f#v (fold (fold i f x) f y) t
let v =
object method v : type a. _ -> a Gadt.term -> _ =
fun x -> function
| Int n -> x+n
| Add -> x+1
| App _ -> x+2
end
let r = Gadt.fold 0 v (App (App (Add, Int 3), Int 5))
The point being that to match on a Gadt you will anyway need to use the
(type a) construct to allow refinement.
Jacques
On 08/01/2020 07:54, rixed@happyleptic.org wrote:
> Hello and thank you for the answer.
>
> On Tue, Jan 7, 2020, at 21:21, Ivan Gotovchits wrote:
>> It is the limitation of the let-bound polymorphism. (...)
>> In your case, I would define a visitor type, e.g.,
>> type 'r visitor = {visit : 'a. 'a term -> 'r -> 'r}
> Oh I see. I've used this trick to force a function to be polymorphic, but I failed to see that this was the problem because to me `f` is not any more polymorphic when the `term` is a GADT than when it's not.
>
> So there is no lighter syntax to specify that `f` should accept any member of a GADT than the syntax to specify that `f` should accept any type at all?
>
> I wonder, is this just a limitation of the OCaml parser or is there some deep reason for these work-around (like is the case, from my understanding, for the value restriction)?
>
> Sorry for asking such simple questions but I've build a mental model of how OCaml type checking works mostly from trials and errors, which used to work great until some versions ago :)
```

[-- Attachment #1: Type: text/plain, Size: 6661 bytes --] On Wed, Jan 8, 2020 at 1:54 AM <rixed@happyleptic.org> wrote: > Hello and thank you for the answer. > > On Tue, Jan 7, 2020, at 21:21, Ivan Gotovchits wrote: > > It is the limitation of the let-bound polymorphism. (...) > > In your case, I would define a visitor type, e.g., > > type 'r visitor = {visit : 'a. 'a term -> 'r -> 'r} > > Oh I see. I've used this trick to force a function to be polymorphic, but > I failed to see that this was the problem because to me `f` is not any more > polymorphic when the `term` is a GADT than when it's not. > > So there is no lighter syntax to specify that `f` should accept any member > of a GADT than the syntax to specify that `f` should accept any type at all? > Only three methods of introducing rank-2 polymorphism are known to me: 1. records 2. objects 3. first-class modules Jacques has demonstrated the solution with objects, which might be a little bit more lightweight, at least as you don't need to define a new data type beforehand. But the invocation is more verbose and requires an annotation from the caller side, which could be confusing. The third solution relies on first-class modules and is even more verbose, at least on the definition side. Just for the sake of completeness, module type Visitor = sig type t val term : t -> 'a term -> t end let rec fold : type a r. r -> (module Visitor with type t = r) -> a term -> r = fun i ((module Visit) as f) t -> match t with | Int _ as t -> Visit.term i t | Add as t -> Visit.term i t | App (x,y) as t -> let i = fold i f x in let i = fold i f y in Visit.term i t let s = fold 0 (module struct type t = int let term x _ = x + 1 end) And again, it is not about GADT. GADT act as a red herring here. As I've demonstrated earlier, using a simple pair will suffice to display the limitation of the prenex polymorphism. Even no ADT is required, just apply one term to another two and you will get them unified, e.g., let f g x y : unit = g x; g y will have type val f : ('a -> unit) -> 'a -> 'a -> unit because 'a is quantified on the scope of `f` not `g`, in other words, it has type (not an OCaml syntax) val f : forall 'a. ('a -> unit) -> 'a -> 'a -> unit while we would like to have a type val f : forall 'b, 'c. (forall 'a. 'a -> unit) -> 'b -> 'c -> unit OCaml doesn't allow us to define types like `('a. 'a -> 'a)` and the reason is not that it is hard to extend the parser it is... I wonder, is this just a limitation of the OCaml parser or is there some > deep reason for these work-around (like is the case, from my understanding, > for the value restriction)? Yep, good catch! It is because of the impurity. Indeed, Haskell has the Rank2Types extension that lets us write types like `(forall a. a -> ()) -> b -> c -> ()`, with no extra syntactic burden (modulo having to provide the type annotation). But functions in Haskell are pure, therefore it is possible. To make the story short and obvious, let me do a simple demonstration of how things can go wrong in a language with side-effects. Let's go back to the simple example of pairs and the identity function. Consider the following nasty identity function, let bad_id () = let cache = ref None in fun x -> match cache.contents with | None -> cache := Some x; x | Some cache -> cache It has type `unit -> 'a -> 'a` therefore, if we would have the rank-1 polymorphism enabled for functions, we could apply it to the function let map2 : fun ('a. 'a -> 'a) -> 'b -> 'c -> 'b * 'c = fun f (x,y) -> f x, f y as let x,y : string * int = map2 (bad_id ()) "hello", 42 and will get a segmentation fault, as `y` will now have type int but hold a string. And here comes the syntax as a savior as it lets us specify functions that are guaranteed to be syntactic values. Indeed, all three solutions syntactically guarantee that the provided argument is a function, not a closure. Indeed, let's introduce the universal identity via a record, type id = { f : 'a. 'a -> 'a} and we can see that our `bad_id` is not accepted due to the value restriction, while good_id, defined as, let good_id x = x is perfectly fine, e.g., let id1 = {f = good_id} (*accepted *) let id2 = {f = bad_id} (* rejected *) moreover, even a fine, but not syntactic, identity is also rejected let fine_id () x = x let id3 = {f = fine_id ()} (* rejected *) with the message This field value has type 'b -> 'b which is less general than 'a. 'a -> 'a The same is true with modules, module type Id = sig val f : 'a -> 'a end module Id1 : Id = struct let f = good_id end (* accepted *) module Id2 : Id = struct let f = bad_id () end (* rejected *) module Id3 : Id = struct let f = fine_id () end (* rejected *) and with objects (left as an exercise). To summarize, in order to enable rank2 polymorphism we need a special kind of values to bear universal functions, as we can't rely on ordinary functions, which could be constructed using partial application. OCaml already had objects and records, which serve as a fine media for universally quantified functions. Later first class modules were introduced, which could also be used for the same purpose. Probably, one could devise a special syntax (or rely on the new attributes and extensions syntax, e.g., `map2 [%rank2 : fun x -> x] ("hello",42)` but probably this will lead to an unnecessary bloating of the language and the implementation, especially since we already have three solutions with a more or less tolerable syntax (and are in the base language, not an extension). Besides, if we will use the `[@@unboxed]` annotation, or visitor will have the same representation as a function, e.g., type 'r visitor = {visit : 'a. 'r -> 'a term -> 'r} [@@unboxed] let count x _ = x + 1 let counter = {visit=count} and # Core_kernel.phys_same count counter;; - : bool = true Concerning rank-n polymorphism, in OCaml is is achieved using functors. Yes, they are a little bit syntactically heavy and force us to write signatures, but this is necessary anyway as rank-n is undecidable (non-inferrable). Finally, as a real-world example [1] of rank-2 polymorphism consider the universal WAVL tree that is a binary tree with each element having a different type (aka heterogeneous map). We use it in BAP as a backing store. You might find a few tricks there, especially using continuation-passing in the recursive cases. Cheers, Ivan [1]: https://github.com/BinaryAnalysisPlatform/bap/blob/b40689e636607b977758af048b79d65684ce48c3/lib/knowledge/bap_knowledge.ml#L847-L1693 [-- Attachment #2: Type: text/html, Size: 9009 bytes --] <div dir="ltr"><div dir="ltr"><br></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Jan 8, 2020 at 1:54 AM <<a href="mailto:rixed@happyleptic.org">rixed@happyleptic.org</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Hello and thank you for the answer.<br> <br> On Tue, Jan 7, 2020, at 21:21, Ivan Gotovchits wrote:<br> > It is the limitation of the let-bound polymorphism. (...)<br> > In your case, I would define a visitor type, e.g.,<br> > type 'r visitor = {visit : 'a. 'a term -> 'r -> 'r}<br> <br> Oh I see. I've used this trick to force a function to be polymorphic, but I failed to see that this was the problem because to me `f` is not any more polymorphic when the `term` is a GADT than when it's not.<br> <br> So there is no lighter syntax to specify that `f` should accept any member of a GADT than the syntax to specify that `f` should accept any type at all?<br> </blockquote><div><br></div><div>Only three methods of introducing rank-2 polymorphism are known to me:<br></div><div>1. records</div><div>2. objects</div><div>3. first-class modules</div><div><br></div><div>Jacques has demonstrated the solution with objects, which might be a little bit more lightweight, at least as you don't need to define a new data type beforehand. But the invocation is more verbose and requires an annotation from the caller side, which could be confusing. The third solution relies on first-class modules and is even more verbose, at least on the definition side. Just for the sake of completeness,</div><div><br></div><div> module type Visitor = sig<br> type t<br> val term : t -> 'a term -> t<br> end<br><br> let rec fold : type a r. r -> (module Visitor with type t = r) -> a term -> r =<br> fun i ((module Visit) as f) t -> match t with<br> | Int _ as t -> Visit.term i t<br> | Add as t -> Visit.term i t<br> | App (x,y) as t -><br> let i = fold i f x in<br> let i = fold i f y in<br> Visit.term i t<br><br> let s = fold 0 (module struct<br> type t = int<br> let term x _ = x + 1<br> end)<br></div><div><br></div><div>And again, it is not about GADT. GADT act as a red herring here. As I've demonstrated earlier, using a simple pair will suffice to display the limitation of the prenex polymorphism. Even no ADT is required, just apply one term to another two and you will get them unified, e.g.,</div><div><br></div><div> let f g x y : unit = g x; g y</div><div><br></div><div>will have type</div><div><br></div><div> val f : ('a -> unit) -> 'a -> 'a -> unit</div><div><br></div><div>because 'a is quantified on the scope of `f` not `g`, in other words, it has type (not an OCaml syntax) </div><div><br></div><div> val f : forall 'a. ('a -> unit) -> 'a -> 'a -> unit</div><div><br></div><div>while we would like to have a type</div><div><br></div><div> val f : forall 'b, 'c. (forall 'a. 'a -> unit) -> 'b -> 'c -> unit</div><div><br></div><div>OCaml doesn't allow us to define types like `('a. 'a -> 'a)` and the reason is not that it is hard to extend the parser it is...</div><div><br></div><div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"> I wonder, is this just a limitation of the OCaml parser or is there some deep reason for these work-around (like is the case, from my understanding, for the value restriction)?</blockquote><div><br></div><div>Yep, good catch! It is because of the impurity. Indeed, Haskell has the Rank2Types extension that lets us write types like `(forall a. a -> ()) -> b -> c -> ()`, with no extra syntactic burden (modulo having to provide the type annotation). But functions in Haskell are pure, therefore it is possible. To make the story short and obvious, let me do a simple demonstration of how things can go wrong in a language with side-effects. Let's go back to the simple example of pairs and the identity function. Consider the following nasty identity function, <br></div><div><br></div><div> let bad_id () =<br> let cache = ref None in<br> fun x -> match cache.contents with<br> | None -> cache := Some x; x<br> | Some cache -> cache<br></div><div><br></div><div>It has type `unit -> 'a -> 'a` therefore, if we would have the rank-1 polymorphism enabled for functions, we could apply it to the function</div><div><br></div><div> let map2 : fun ('a. 'a -> 'a) -> 'b -> 'c -> 'b * 'c = fun f (x,y) -> f x, f y</div><div><br></div><div>as</div><div><br></div><div> let x,y : string * int = map2 (bad_id ()) "hello", 42</div><div><br></div><div>and will get a segmentation fault, as `y` will now have type int but hold a string.</div><div><br></div><div>And here comes the syntax as a savior as it lets us specify functions that are guaranteed to be syntactic values. Indeed, all three solutions syntactically guarantee that the provided argument is a function, not a closure. Indeed, let's introduce the universal identity via a record,</div><div><br></div><div> type id = { f : 'a. 'a -> 'a}<br></div><div><br></div><div>and we can see that our `bad_id` is not accepted due to the value restriction, while good_id, defined as,</div><div><br></div><div> let good_id x = x</div><div><br></div><div>is perfectly fine, e.g.,</div><div><br></div><div> let id1 = {f = good_id} (*accepted *)<br> let id2 = {f = bad_id} (* rejected *)<br></div><div><br></div><div>moreover, even a fine, but not syntactic, identity is also rejected </div><div><br></div><div> let fine_id () x = x</div><div> let id3 = {f = fine_id ()} (* rejected *)<br></div><div><br></div><div>with the message</div><div><br></div><div> This field value has type 'b -> 'b which is less general than 'a. 'a -> 'a<br></div><div><br></div><div>The same is true with modules,</div><div><br></div><div> module type Id = sig<br> val f : 'a -> 'a<br> end<br> module Id1 : Id = struct let f = good_id end (* accepted *)<br> module Id2 : Id = struct let f = bad_id () end (* rejected *)<br> module Id3 : Id = struct let f = fine_id () end (* rejected *)<br></div><div><br></div><div>and with objects (left as an exercise).</div><div><br></div><div>To summarize, in order to enable rank2 polymorphism we need a special kind of values to bear universal functions, as we can't rely on ordinary functions, which could be constructed using partial application. OCaml already had objects and records, which serve as a fine media for universally quantified functions. Later first class modules were introduced, which could also be used for the same purpose. Probably, one could devise a special syntax (or rely on the new attributes and extensions syntax, e.g., `map2 [%rank2 : fun x -> x] ("hello",42)` but probably this will lead to an unnecessary bloating of the language and the implementation, especially since we already have three solutions with a more or less tolerable syntax (and are in the base language, not an extension). Besides, if we will use the `[@@unboxed]` annotation, or visitor will have the same representation as a function, e.g.,</div><div><br></div><div> type 'r visitor = {visit : 'a. 'r -> 'a term -> 'r} [@@unboxed]</div><div> let count x _ = x + 1</div><div> let counter = {visit=count} </div><div><br></div><div>and</div><div><br></div><div> # Core_kernel.phys_same count counter;;</div> - : bool = true<div><br></div><div>Concerning rank-n polymorphism, in OCaml is is achieved using functors. Yes, they are a little bit syntactically heavy and force us to write signatures, but this is necessary anyway as rank-n is undecidable (non-inferrable). Finally, as a real-world example [1] of rank-2 polymorphism consider the universal WAVL tree that is a binary tree with each element having a different type (aka heterogeneous map). We use it in BAP as a backing store. You might find a few tricks there, especially using continuation-passing in the recursive cases. </div><div><br></div><div>Cheers,</div><div>Ivan</div><div><br></div><div><br></div><div>[1]: <a href="https://github.com/BinaryAnalysisPlatform/bap/blob/b40689e636607b977758af048b79d65684ce48c3/lib/knowledge/bap_knowledge.ml#L847-L1693">https://github.com/BinaryAnalysisPlatform/bap/blob/b40689e636607b977758af048b79d65684ce48c3/lib/knowledge/bap_knowledge.ml#L847-L1693</a></div><div><br></div><div> </div><div><br></div><div><br></div><div></div></div></div></div>

Thank you for the explanation Ivan. I have two questions inline. Ivan Gotovchits <ivg@ieee.org> writes: > It has type `unit -> 'a -> 'a` therefore, if we would have the rank-1 > polymorphism enabled for functions, we could apply it to the function > > let map2 : fun ('a. 'a -> 'a) -> 'b -> 'c -> 'b * 'c = fun f (x,y) -> > f x, f y Small thing, but wouldn't the faux type be the following, based on your usage (making sure I'm following): fun ('a. 'a -> 'a) -> ('b * 'c) -> 'b * 'c > as > > let x,y : string * int = map2 (bad_id ()) "hello", 42 > > and will get a segmentation fault, as `y` will now have type int but hold a > string. > > And here comes the syntax as a savior as it lets us specify functions that > are guaranteed to be syntactic values. Indeed, all three solutions > syntactically guarantee that the provided argument is a function, not a > closure. Indeed, let's introduce the universal identity via a record, > > type id = { f : 'a. 'a -> 'a} > > and we can see that our `bad_id` is not accepted due to the value > restriction, while good_id, defined as, > > let good_id x = x > > is perfectly fine, e.g., > > let id1 = {f = good_id} (*accepted *) > let id2 = {f = bad_id} (* rejected *) > > moreover, even a fine, but not syntactic, identity is also rejected > > let fine_id () x = x > let id3 = {f = fine_id ()} (* rejected *) > > with the message > > This field value has type 'b -> 'b which is less general than 'a. 'a -> 'a > Why is type checking creating a record different than type checking a function argument? If we had the syntax (or something like it): let map2 : ('a. 'a -> 'a) -> ('b * 'c) -> ('b * 'c) Why would the type checker not be able to see that map2 good_id ("hi", 42) is valid but map2 (fine_id ()) ("hi", 32) is not, using the same logic that is verifying creating the "id" record is not valid?

[-- Attachment #1: Type: text/plain, Size: 3519 bytes --] On Fri, Jan 10, 2020 at 4:50 AM Malcolm Matalka <mmatalka@gmail.com> wrote: > Thank you for the explanation Ivan. I have two questions inline. > > Ivan Gotovchits <ivg@ieee.org> writes: > > > It has type `unit -> 'a -> 'a` therefore, if we would have the rank-1 > > polymorphism enabled for functions, we could apply it to the function > > > > let map2 : fun ('a. 'a -> 'a) -> 'b -> 'c -> 'b * 'c = fun f (x,y) > -> > > f x, f y > > Small thing, but wouldn't the faux type be the following, based on your > usage (making sure I'm following): > > fun ('a. 'a -> 'a) -> ('b * 'c) -> 'b * 'c > Yep, sure :) That's the problem with faux-typing) > Why is type checking creating a record different than type checking a > function argument? > > If we had the syntax (or something like it): > > let map2 : ('a. 'a -> 'a) -> ('b * 'c) -> ('b * 'c) > > Why would the type checker not be able to see that > > map2 good_id ("hi", 42) > > is valid but > > map2 (fine_id ()) ("hi", 32) > > is not, using the same logic that is verifying creating the "id" record > is not valid? > I believe it is possible, as it is possible in Haskell (with RankNTypes and ScopedTypeVariables). The main (theoretical) difference is that in OCaml we need to check whether an expression is expansive and use a specialized generalization in case if it is (for the relaxed value restriction). It will, however, complicate the type inference engine a lot, but most importantly, changing the typing rule of functions will have a tremendous impact on the language. So this would be a very impractical solution. Especially, since we don't have the mechanism of language extensions, enabling RankNTypes will make a lot of programs untypeable, as they will now require type annotations (recall that RankN is undecidable in general). It could probably be implemented as a compiler command line parameter, like `-rectypes` but this will be still quite impractical since more often code like `fun f -> f 1, f true` is a programmer error, rather than a true request for universal polymorphism (the same as with rectypes, recursive types a more often an error rather than a deliberate attempt). Therefore, enabling RankN(^1) polymorphism will type too many programs (not that it is unsound, just many programs won't have sense) at the cost of even more obscure type errors. On the other hand, we have three syntactic constructs that let us express non-prenex polymorphism of the necessary rank(^2) without breaking anything else. So it looks like a good deal - we can have rankN polymorphism and decidable type checker at the same time. Just think of polymorphic records/methods as an embedded DSL for rankN polymorphism. ============ Footnotes: 1) An important point, that I forgot to notice, is that enabling scoped type variables, will inevitably enable rankN polymorphism, e.g., since now any type could be a polytype, then suppose we have type `'a. ('b.'b -> 'a) -> 'a` could be instantiated to 'a = 'd. ('c. -> 'd) -> 'd, so that our type is now `'d. ('b. 'b -> ('c. 'c -> 'd) -> 'd) -> ('c. 'c -> 'd) -> 'd` which is now rank3. Therefore, enabling arbitrary quantification in the arrow type will lead to rankN and immediately make undecidable most of the type checker. 2) We can craft arbitrary rank using records with universally quantified type variables, e.g., here is an example of rank3 polymoprhism: type 'a rank1 = {f1 : 's. 's -> 'a} type 'a rank2 = {f2 : 'r. 'r -> 'a rank1} Indeed, `f2` has type `'a.('r. 'r -> ('s. 's -> 'a)` [-- Attachment #2: Type: text/html, Size: 4704 bytes --] <div dir="ltr"><div dir="ltr"><br></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Jan 10, 2020 at 4:50 AM Malcolm Matalka <<a href="mailto:mmatalka@gmail.com">mmatalka@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Thank you for the explanation Ivan. I have two questions inline.<br> <br> Ivan Gotovchits <<a href="mailto:ivg@ieee.org" target="_blank">ivg@ieee.org</a>> writes:<br> <br> > It has type `unit -> 'a -> 'a` therefore, if we would have the rank-1<br> > polymorphism enabled for functions, we could apply it to the function<br> ><br> > let map2 : fun ('a. 'a -> 'a) -> 'b -> 'c -> 'b * 'c = fun f (x,y) -><br> > f x, f y<br> <br> Small thing, but wouldn't the faux type be the following, based on your<br> usage (making sure I'm following):<br> <br> fun ('a. 'a -> 'a) -> ('b * 'c) -> 'b * 'c<br></blockquote><div><br></div><div>Yep, sure :) That's the problem with faux-typing) </div><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"> <br> Why is type checking creating a record different than type checking a<br> function argument?<br> <br> If we had the syntax (or something like it):<br> <br> let map2 : ('a. 'a -> 'a) -> ('b * 'c) -> ('b * 'c)<br> <br> Why would the type checker not be able to see that<br> <br> map2 good_id ("hi", 42)<br> <br> is valid but<br> <br> map2 (fine_id ()) ("hi", 32)<br> <br> is not, using the same logic that is verifying creating the "id" record<br> is not valid?<br></blockquote><div><br></div><div>I believe it is possible, as it is possible in Haskell (with RankNTypes and ScopedTypeVariables). The main (theoretical) difference is that in OCaml we need to check whether an expression is expansive and use a specialized generalization in case if it is (for the relaxed value restriction). It will, however, complicate the type inference engine a lot, but most importantly, changing the typing rule of functions will have a tremendous impact on the language. So this would be a very impractical solution. Especially, since we don't have the mechanism of language extensions, enabling RankNTypes will make a lot of programs untypeable, as they will now require type annotations (recall that RankN is undecidable in general). It could probably be implemented as a compiler command line parameter, like `-rectypes` but this will be still quite impractical since more often code like `fun f -> f 1, f true` is a programmer error, rather than a true request for universal polymorphism (the same as with rectypes, recursive types a more often an error rather than a deliberate attempt). Therefore, enabling RankN(^1) polymorphism will type too many programs (not that it is unsound, just many programs won't have sense) at the cost of even more obscure type errors. On the other hand, we have three syntactic constructs that let us express non-prenex polymorphism of the necessary rank(^2) without breaking anything else. So it looks like a good deal - we can have rankN polymorphism and decidable type checker at the same time. Just think of polymorphic records/methods as an embedded DSL for rankN polymorphism.</div><div><br></div><div>============</div><div>Footnotes:</div><div><br></div><div>1) An important point, that I forgot to notice, is that enabling scoped type variables, will inevitably enable rankN polymorphism, e.g., since now any type could be a polytype, then suppose we have type `'a. ('b.'b -> 'a) -> 'a` could be instantiated to 'a = 'd. ('c. -> 'd) -> 'd, so that our type is now `'d. ('b. 'b -> ('c. 'c -> 'd) -> 'd) -> ('c. 'c -> 'd) -> 'd` which is now rank3. Therefore, enabling arbitrary quantification in the arrow type will lead to rankN and immediately make undecidable most of the type checker.</div><div><br></div><div>2) We can craft arbitrary rank using records with universally quantified type variables, e.g., here is an example of rank3 polymoprhism:</div><div><br></div><div> type 'a rank1 = {f1 : 's. 's -> 'a}<br> type 'a rank2 = {f2 : 'r. 'r -> 'a rank1}<br></div><div><br></div><div>Indeed, `f2` has type `'a.('r. 'r -> ('s. 's -> 'a)`</div></div></div>