Re: [Caml-list] GADT magic

[Gabriel Scherer <gabriel.scherer@gmail.com>]

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