Question about type unification

Question about type unification

[Richard Jones]

With this definition:

  type 'a t = float

Why is this allowed?

  # ((3.0 : unit t) : string t) ;;
  - : string t = 3.

Note that unification is prevented if t is opaque, eg, hidden behind a
module signature.

Rich.

-- 
Richard Jones
Red Hat

Re: [Caml-list] Question about type unification

[Jon Harrop]

On Monday 26 May 2008 13:22:04 Richard Jones wrote:
> With this definition:
>
>   type 'a t = float
>
> Why is this allowed?
>
>   # ((3.0 : unit t) : string t) ;;
>   - : string t = 3.
>
> Note that unification is prevented if t is opaque, eg, hidden behind a
> module signature.

Because your accessible definition allows you to replace 'a t with float for 
any 'a, which allows you to replace both of your types with float and, 
therefore, they must unify.

-- 
Dr Jon D Harrop, Flying Frog Consultancy Ltd.
http://www.ffconsultancy.com/products/?e

Re: [Caml-list] Question about type unification

[Romain Bardou]

Richard Jones a écrit :
> With this definition:
> 
>   type 'a t = float
> 
> Why is this allowed?
> 
>   # ((3.0 : unit t) : string t) ;;
>   - : string t = 3.
> 
> Note that unification is prevented if t is opaque, eg, hidden behind a
> module signature.
> 
> Rich.
> 

My guess is that 'a t being just a type abbreviation, it is expanded to 
float when unifying. Private types are not type abbreviations, so they 
can't be expanded.

-- 
Romain Bardou

Re: [Caml-list] Question about type unification

[Fabrice Marchant]

On Mon, 26 May 2008 13:22:04 +0100
Richard Jones <rich@annexia.org> wrote:

> 
> With this definition:
> 
>   type 'a t = float
> 
> Why is this allowed?
> 
>   # ((3.0 : unit t) : string t) ;;
>   - : string t = 3.

  Never thought to write such odd things. Maybe is there some interesting use ?

Fabrice

Re: [Caml-list] Question about type unification

[Robert Fischer]

How is the compiler magically getting from the float to a string value?  Can someone break down
what's actually happening here for me?

~~ Robert.

Fabrice Marchant wrote:
> On Mon, 26 May 2008 13:22:04 +0100
> Richard Jones <rich@annexia.org> wrote:
> 
>> With this definition:
>>
>>   type 'a t = float
>>
>> Why is this allowed?
>>
>>   # ((3.0 : unit t) : string t) ;;
>>   - : string t = 3.
> 
>   Never thought to write such odd things. Maybe is there some interesting use ?
> 
> Fabrice
> 
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
> 

Re: [Caml-list] Question about type unification

[DooMeeR]

Robert Fischer a écrit :
> How is the compiler magically getting from the float to a string value?  Can someone break down
> what's actually happening here for me?

It's not "getting to" a "string" value but to a "string t" value, which 
is an abbreviation for "float". The value has type "float", but the user 
requires type "string t", so the compiler unifies "float" and "string t" 
which is actually "float" so it's ok, and then the compiler gives the 
type requested by the user to the value, i.e., "string t".

Well, at least, this is how I understand this :)

-- 
Romain Bardou

Re: [Caml-list] Question about type unification

[Robert Fischer]

Ahh.  Yeah, I see it now -- the output wasn't a string, but a float.  It just has the word "string"
in the type name to confuse me.

~~ Robert.

DooMeeR wrote:
> Robert Fischer a écrit :
>> How is the compiler magically getting from the float to a string
>> value?  Can someone break down
>> what's actually happening here for me?
> 
> It's not "getting to" a "string" value but to a "string t" value, which
> is an abbreviation for "float". The value has type "float", but the user
> requires type "string t", so the compiler unifies "float" and "string t"
> which is actually "float" so it's ok, and then the compiler gives the
> type requested by the user to the value, i.e., "string t".
> 
> Well, at least, this is how I understand this :)
> 

Re: [Caml-list] Question about type unification

[Jeremy Yallop]

Robert Fischer wrote:
> How is the compiler magically getting from the float to a string value?  Can someone break down
> what's actually happening here for me?

Type aliases are analogous to functions.  If you have a variable "f" 
that denotes a pure function and some values u1 ... un and v1 ... vn 
then to determine whether

    f u1 ... un

is equal to

    f v1 ... vn

you call the function (twice) by substituting u1 ... un and v1 ... vn 
for the parameters.  If you have a constant function

    f = fun _ ... _ = v

then any application of the function will give the same result (v) 
regardless of the values of the arguments.  Analogously, if you have a 
type constructor "t" that denotes a type alias and some types s1 ... sn 
and t1 ... tn then to determine whether

    (s1, ... sn) t

is equal to

    (t1, ... tn) t

you "call" the type alias by substituting s1 ... sn and t1 ... tn for 
the type parameters.  If you have a "constant" type alias in which none 
of the type parameters appear on the right hand side of the definition

    type ('a1, ... 'an) t = e            a1...an not in fv(e)

then any application of the type constructor will give the same result 
(e) regardless of the values of the arguments.

Nominal types are analogous to constructors.  (By "nominal" I mean 
record and sum types, or types made abstract using a module signature.) 
  If you have a data constructor "C" and some values u1 ... un and v1 
... vn then to determine whether

    C u1 ... un

is equal to

    C v1 ... vn

you check whether ui is equal to vi for each i.  Analogously, if you 
have a type constructor "s" that denotes a nominal type and some types 
s1 ... sn and t1 ... tn then to determine whether

    (s1, ... sn) s

is equal to

    (t1, ... tn) s

you check whether si is equal to ti for each i.

In Richard's example "t" denotes a type alias.  Thus to determine whether

   unit t

is equal to

   string t

we look at the definition of t:

   type 'a t = float

then replace each 'a that occurs on the right hand side first with 
"unit" and then with "string" and compare the results.  In this case 
"'a" doesn't appear at all on the right hand side of the definition so 
we compare "float" with "float", and find that the two are equal, i.e. 
"unit t" and "string t" denote the same type (float).

Jeremy.

Re: [Caml-list] Question about type unification

[Richard Jones]

Yes, they are the basis of phantom types:

http://camltastic.blogspot.com/2008/05/phantom-types.html

Rich.

-- 
Richard Jones
Red Hat