Accueil     Ŕ propos     Téléchargement     Ressources     Contactez-nous

Ce site est rarement mis ŕ jour. Pour les informations les plus récentes, rendez-vous sur le nouveau site OCaml ŕ l'adresse ocaml.org.

Re: Typing problem
• j h woodyatt
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
 Date: 2006-03-19 (14:24) From: j h woodyatt Subject: Re: Typing problem
```Daniel Bünzli <daniel.buenzli@epfl.ch>
>
> I would like to define the following types.
>
>> type u = [ `U1 | `U2 ]
>> type 'a t = [`A of 'a | `B of ([`U1 ] as 'a) ] constraint 'a = [< u ]
>
> t's parameter is used to statically express constraints in other
> parts of the code. My problem is that the constraint on 'a is
> downgraded to [`U1] while I would like to be able to write
>
>> let param : 'a t -> 'a = function (`A v | `B v) -> v
>
> and get the following typing behaviour.
>
>> let v = param (`A `U1) (* should type *)
>> let v = param (`A `U2) (* should type *)
>> let v = param (`B `U1) (* should type *)
>> let v = param (`B `U2) (* should not type *)
>
> Is it possible to express that in ocaml's type system ?

The short answer is no.  The reason is that 'a is not the same type
in the `A case as in the `B case.  Type t really has two type
parameters.  (Well, it can have only one if this contrived example is
fully representative of your code, as I'll describe below).

type ('a, 'b) t = [ `A of 'a | `B of 'b ]
constraint 'a = [< u ] constraint 'b = [ `U1 ]

However, 'b is concrete in your example, so-- if it's fully
representative of your code-- you could just do this, and you would
still have only one type parameter:

type 'a t = [ `A of 'a | `B of [ `U1 ] ]
constraint 'a = [< u ]

—
j h woodyatt <jhw@conjury.org>

```