[Caml-list] GADT magic

[Caml-list] GADT magic

[Rodolphe Lepigre]

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/

Re: [Caml-list] GADT magic

[Gabriel Scherer]

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?)

Have you considered using polymorphic variants? They were designed for
this use-case, see for example

  Code reuse through polymorphic variants.
  Jacques Garrigue, 2000
  http://www.math.nagoya-u.ac.jp/~garrigue/papers/variant-reuse.pdf

  Le caractère ` à la rescousse - Factorisation et réutilisation de
code grâce aux variants polymorphes
  Boris Yakobowski, 2008
  http://gallium.inria.fr/~yakobows/publis/2008/jfla08.pdf

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

Re: [Caml-list] GADT magic

[Jacques Garrigue]

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