Re: [Caml-list] Type of term

[Goswin von Brederlow <goswin-v-b@web.de>]

On Thu, Feb 06, 2014 at 05:32:00PM +0000, Mário José Parreira Pereira wrote:
> Hi Lukasz,
> 
> Thank you for your answer but I really can't see how GADTs can help me.
> 
> I was just simply wandering if there wasn't any OCaml function that
> would work like:
>    type_of(let f x = x) = 'a->'a
> 
> There is, something that would compute exactly the same outcome as
> the Damas-Milner algorithm W.
> 
> Bests,
> Mário
> 
> Em 06-02-2014 17:17, Lukasz Stafiniak escreveu:
> >On Thu, Feb 6, 2014 at 6:17 PM, Mário José Parreira Pereira
> ><mariojppereira@gmail.com <mailto:mariojppereira@gmail.com>>
> >wrote:
> >
> >    Hi all,
> >
> >    Is there any way to get the type of (part of) a program? Something
> >    like:
> >       type_of(M) = sigma
> >    computing the type of program M as sigma so I can pattern match it.
> >
> >
> >No. However, if you really need this rather than being confused by
> >programming patterns from Java / C# / C++, you should learn about
> >GADTs.
> >http://caml.inria.fr/pub/docs/manual-ocaml-400/manual021.html#toc85
> >
> >Cheers.

# let f x = x;;
val f : 'a -> 'a = <fun>
# let g = (f : 'a -> 'a);;
val g : 'a -> 'a = <fun>

But this only unifies the types:

# let f x = x + 1;;
val f : int -> int = <fun>
# let g = (f : 'a -> 'a);;
val g : int -> int = <fun>

To test for equality you need to use a module with signature (or .mli file):

# module M : sig val g : 'a -> 'a end = struct let g = f end;;
Error: Signature mismatch:
       Modules do not match:
         sig val g : int -> int end
       is not included in
         sig val g : 'a -> 'a end
       Values do not match:
         val g : int -> int
       is not included in
         val g : 'a -> 'a


If you don't want a static compile time check then GADTs are the way
to go. With GADTs you can construct runtime type informations, pass
them as values and match on them. But you would have to construct the
GADTs for every function you may want to type_of() or use a
preprocessor module to do so implicitly. I think there is also a ocaml
branch that adds such type values implicitly in the compiler.

MfG
	Goswin