Version française
Home     About     Download     Resources     Contact us    
Browse thread
Typing of patterns
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Jacques Garrigue <garrigue@k...>
Subject: Re: Typing of patterns
From: Patrick M Doane <patrick@watson.org>

> I want to change the data associated to a particular constructor of a
> variant and leave the others unmodified:
> 
>      # let f = function `A -> `A () | _ as t -> t;;
>      Characters 41-42:
>      This expression has type [< `A | ..] but is here used with type
>        [> `A of unit]
> 
> Notice that the type for '_' includes `A when it obviously cannot. One
> could include every possible expected type in place of '_' but that
> removes one of the advantages of polymorphic variants: that the type can 
> be refined and extended easily.

However, this is what you will have to do :-)
I know that it is theoretically possible to build a type system
where t is given a type excluding `A, but this would require exposing
the row variable, which we have been carefully avoiding until now.

As for the ease of definition, you can use type-patterns:

type others = [ you other cases ]
let f = function `A -> `A () | #others as t -> t

I believe this should be enough in general.

> While further exploring this issue I managed to get an uncaught exception
> from the type checker:
> 
>      # let f = function `A true -> () | `A 5 -> ();; 
>      Uncaught exception: File "typing/parmmatch.ml", ...

This is a known bug, the current version of the typechecker finds an
error here,

> Taking the conjuction of 'unit' and 'int' does seem to work however,
> 
>      # let f = function `A -> () | `A 5 -> ();;
>      val f : [< `A of & int] -> unit = <fun>

and also here (basically conflicting types are not allowed in the same
pattern-matching).

        Jacques