* Re: [Caml-list] Type of term
2014-02-06 17:32 ` Mário José Parreira Pereira
@ 2014-02-06 17:45 ` Raphaël Proust
2014-02-06 19:01 ` Gabriel Scherer
2014-02-10 8:58 ` Goswin von Brederlow
2 siblings, 0 replies; 8+ messages in thread
From: Raphaël Proust @ 2014-02-06 17:45 UTC (permalink / raw)
To: Mário José Parreira Pereira; +Cc: caml-list
$ echo "let f x = x;;" | ocaml | grep ':' | sed 's/^.*: //' | sed 's/ =.*//'
'a -> 'a
(Replace `let f x = x` with any ocaml expression.)
More seriously, you might want to have a look at the compiler libs.
On Thu, Feb 6, 2014 at 5:32 PM, Mário José Parreira Pereira
<mariojppereira@gmail.com> 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> 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.
>
>
--
______________
Raphaël Proust
^ permalink raw reply [flat|nested] 8+ messages in thread
* Re: [Caml-list] Type of term
2014-02-06 17:32 ` Mário José Parreira Pereira
2014-02-06 17:45 ` Raphaël Proust
@ 2014-02-06 19:01 ` Gabriel Scherer
2014-02-06 19:05 ` Simon Cruanes
2014-02-10 8:58 ` Goswin von Brederlow
2 siblings, 1 reply; 8+ messages in thread
From: Gabriel Scherer @ 2014-02-06 19:01 UTC (permalink / raw)
To: Mário José Parreira Pereira; +Cc: Lukasz Stafiniak, caml-list
> I was just simply wandering if there wasn't any OCaml function that would
> work like:
> type_of(let f x = x) = 'a->'a
No, there is not.
What are you trying to do?
On Thu, Feb 6, 2014 at 6:32 PM, Mário José Parreira Pereira
<mariojppereira@gmail.com> 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> 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.
>
>
^ permalink raw reply [flat|nested] 8+ messages in thread
* Re: [Caml-list] Type of term
2014-02-06 17:32 ` Mário José Parreira Pereira
2014-02-06 17:45 ` Raphaël Proust
2014-02-06 19:01 ` Gabriel Scherer
@ 2014-02-10 8:58 ` Goswin von Brederlow
2 siblings, 0 replies; 8+ messages in thread
From: Goswin von Brederlow @ 2014-02-10 8:58 UTC (permalink / raw)
To: caml-list
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
^ permalink raw reply [flat|nested] 8+ messages in thread