Re: [Caml-list] GADT+polymorphic variants quirk

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

On 2017/01/03 23:05, Nils Becker wrote:
> 
> hi,
> 
> i am the OP of the stackoverflow question referred to by anton.
> 
>> I would suggest avoid using polymorphic variants here, using rather
>> a simple encoding:
>> 
>>   type whole = Whole
>>   type general = General
>> 
>>   type _ num =
>>      | I : int -> _ num
>>      | F : float -> general num
> 
> i tried this simpler proposal and it does seem to work nicely. however,
> what i'm really interested in is encoding somewhat more elaborate
> subtyping relationships. for example, how would you handle the case
> where there is a 'rational' number type inbetween integers and reals? i
> don't see how your proposal can be generalized to that?
> 
> i tried to generalize the solution proposed by anton like this:
> 
> type integer = [ `Integer ]
> type rational = [ integer | `Rational ]
> type real = [ rational | `Real ]
> 
> type _ num =
>  | N : int -> [> integer ] num
>  | Q : int * int -> [> rational ] num
>  | R : float -> real num

You can encode any finite set type using core types.
The idea is just to use presence and absence.

type pre = Pre
type abs = Abs

type integer = pre * abs * abs  (* integer * rational * real *)
type rational = pre * pre * abs
type real = pre * pre * pre

However, in this case we are only taking about a linear inheritance hierarchy,
which can be expressed more compactly. For instance

type real = Real
type ’a rat = Rational of ‘a
type rational = int * int rat
type integer = int rat

In general, any linear hierarchy can be encoded using type level natural numbers

type zero = Zero
type ‘a succ = Succ of ‘a

which in this case would give

type real = zero
type rational = zero succ
type integer = zero succ succ

This scheme can be extended to any n-ary tree hierarchy, using a n-ary constructor in place of succ.

Jacques