RE: [Caml-list] problem to use gadt

[David Allsopp <dra-news@metastack.com>]

Nicolas Boulay wrote:
> I try to define my own type system using gadt. 
> But it seems that is complex to mix both type system : mine and the ocaml one.
>
> This tiny example did not compile:
> type _ t =
>  | Or: _ t * _ t -> _ t

Is this definitely what you mean - the "_" is not itself a distinct type variable so all three underscores in this instance are different types. cf the signature of the constructor:

Or : 'b t * 'c -> 'a t

>  | Int : int t
>  | Float : float t
>
> let a = Or (Int, Float)  (*is ok*)

But again, does it have the type you mean, in this case 'a t?

> let (||)  a b = Or (a, b)
> let aa = Int || Float (*Error: '_a t, contains type variable that cannot be generalized*)

This is a consequence of the value restriction, I think.

> Using an operator make a difference. But how to exprime "don't care"
> if a choice between 2 types is not possible to be define.  It could 
> be nice if "('a | 'b) t" worked :) Should i use normal sum type, and
> make all type check by a function ?

So you're saying that you don't care what the type of the two halves of an Or is? I don't see the problem you're trying to solve, but I wonder if your issue is that you need to pick a concrete type representation for the Or constructor. For example, does

Or : _ t * _t -> unit t

solve your problem?

HTH,


David