Browse thread
Binding and evaluation order in module/type/value languages
-
Dawid Toton
-
Jacques Garrigue
- Dawid Toton
-
Jacques Garrigue
[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: | 2010-05-21 (16:02) |
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. Dawid