[Caml-list] Type of term

[Caml-list] Type of term

[Mário José Parreira Pereira]

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.

Best regards,
Mário Pereira

Re: [Caml-list] Type of term

[Lukasz Stafiniak]

[-- Attachment #1: Type: text/plain, Size: 512 bytes --]

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.

[-- Attachment #2: Type: text/html, Size: 1001 bytes --]

Re: [Caml-list] Type of term

[Lukasz Stafiniak]

[-- Attachment #1: Type: text/plain, Size: 591 bytes --]

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.
>
>
Besides GADTs, another thing that comes to mind is "module type of":

http://caml.inria.fr/pub/docs/manual-ocaml-400/manual021.html#toc82

There is even pattern matching to recover a module from a module value
(first-class modules), but it doesn't benefit from knowing the type of the
module.

[-- Attachment #2: Type: text/html, Size: 1120 bytes --]

Re: [Caml-list] Type of term

[Mário José Parreira Pereira]

[-- Attachment #1: Type: text/plain, Size: 941 bytes --]

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.


[-- Attachment #2: Type: text/html, Size: 2262 bytes --]

Re: [Caml-list] Type of term

[Raphaël Proust]

$ 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

Re: [Caml-list] Type of term

[Gabriel Scherer]

> 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.
>
>

Re: [Caml-list] Type of term

[Simon Cruanes]

[-- Attachment #1: Type: text/plain, Size: 350 bytes --]

Le Thu, 06 Feb 2014, Gabriel Scherer a écrit :

> > 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?

Sounds like another use-case for the long-awaited Ocaml-ty extension ;-)

my NaN cents

-- 
Simon

[-- Attachment #2: Type: application/pgp-signature, Size: 819 bytes --]

Re: [Caml-list] Type of term

[Goswin von Brederlow]

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