Re: [Caml-list] GADT magic

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

On 2015/10/03 17:54, Gabriel Scherer wrote:
> 
> This is normal behavior. You rely on the fact, when you write "| t ->
> t", that the remaining case is App which returns a (t term). But the
> type-checker will only learn this fact by opening the App constructor,
> which you do in the "fully explicit" version.
> 
> (The type-checker is already "opening constructors" and exploring
> cases by itself as part of the exhaustiveness/redundancy pattern
> checking that Jacques Garrigue discussed at the OCaml Workshop 2015.
> Jacques, is there any improvement that is possible in this case
> without too much bakctracking?)

Actually, I would have very little hope for the second version of
expr_to_term

let expr_to_term : type a. a expr -> term = function
 | LVar(x)   -> LVar(x)
 | LAbs(f)   -> LAbs(f)
 | t         -> t

The type checking algorithm never tries to infer the possible
values behind a variable pattern, taking into account the other
cases of the pattern-matching. The exhaustiveness check does
it, but it runs after type-checking.

On the other hand, one could consider handling or-patterns:

let expr_to_term : type a. a expr -> term = function
  LVar _ | LAbs _ | Appl _ as t -> t

The idea would be to typecheck each case separately, as somebody
already suggested. Since the result is to turn expr_to_term into
immediate identity, this may be worth considering.
My only concern is that it may not play well with type based optimizations.

Jacques Garrigue

> On Sat, Oct 3, 2015 at 9:02 AM, Rodolphe Lepigre
> <rodolphe.lepigre@univ-savoie.fr> wrote:
>> Dear list,
>> 
>> I am using a GADT and some phantom types to implement an abstract syntax
>> tree for some functional programming language, say the λ-calculus.
>> 
>> My first type definition was something like:
>> 
>> ==========
>> type valu =
>>  | LVar of string
>>  | LAbs of valu -> term
>> and  term =
>>  | Valu of valu
>>  | Appl of term * term
>> ==========
>> 
>> This works fine, but it is annoying to work with because of the coercion
>> constructor "Valu". Then I decided to be to smarter and use some GADT and
>> phantom types:
>> 
>> ==========
>> type v
>> type t
>> 
>> type _ expr =
>>  | LVar : string              -> 'a expr
>>  | LAbs : (v expr -> 'b expr) -> 'a expr
>>  | Appl : 'a expr * 'b expr   ->  t expr
>> 
>> type term = t expr
>> type valu = v expr
>> ==========
>> 
>> This definition is much more convenient since the type "valu" is (kind of)
>> a subtype of the type "term". It is not a real subtype since I had to
>> define a function with the type:
>> 
>> ==========
>> val expr_to_term : type a. a expr -> term
>> ==========
>> 
>> This function is exactly the identity function, but for the type checker
>> to accept it I need to be quite explicit:
>> 
>> ==========
>> let expr_to_term : type a. a expr -> term = function
>>  | LVar(x)   -> LVar(x)
>>  | LAbs(f)   -> LAbs(f)
>>  | Appl(t,u) -> Appl(t,u)
>> ==========
>> 
>> Of course, a better and more efficient implementation for this function
>> is "Obj.magic", but this is not the question here. I was expecting the
>> following definition to work:
>> 
>> ==========
>> let expr_to_term : type a. a expr -> term = function
>>  | LVar(x)   -> LVar(x)
>>  | LAbs(f)   -> LAbs(f)
>>  | t         -> t
>> ==========
>> 
>> But it does not type check. This is weird because all remaining patterns
>> captured by the "t" have type "term"...
>> 
>> Is this normal behaviour? Is this a bug?
>> 
>> Rodolphe
>> --
>> Rodolphe Lepigre
>> LAMA, Université Savoie Mont Blanc, FRANCE
>> http://lama.univ-smb.fr/~lepigre/
>> 
>> --
>> Caml-list mailing list.  Subscription management and archives:
>> https://sympa.inria.fr/sympa/arc/caml-list
>> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
>> Bug reports: http://caml.inria.fr/bin/caml-bugs