Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

Browse thread
Binding and evaluation order in module/type/value languages
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Dawid Toton <d0@w...>
Subject: Re: Binding and evaluation order in module/type/value languages

> It is not clear that this will work at all.
> The semantics of ocaml (contrary to SML) is not defined in terms of
> type generativity.
This is great eureka to me.
I thought that when the compiler refuses to unify some types it knows
that they are incompatible (as the error message says).
But now I think (as I currently understand non-generativity) that
sometimes the compiler simply doesn't know if some types are equal and
avoids unification of such types. The error message should be instead:
"Cannot unify the following types, because I don't have any proof that
they are equal (and I don't have looked for the proof really hard)..."

So in order to have not unifiable phantom types one has to kind of trick
the compiler and hide the fact that they are equal.