[Caml-list] Polymorphic Variants and Number Parameterized Types

[Nadji.Gauthier@lip6.fr]

*disclaimer*
This is a long mail, that probably only polymorphic
variant adepts and static typing fanatics (like me) will like.
Moreover I strongly doubt that it could be very useful.
*end of disclaimer*

Hi list,

recently there was a very interesting mail about encoding 
natural numbers as types for static checking of array sizes,
list length etc..., cf
http://caml.inria.fr/archives/200109/msg00097.html

The trick was to use phantom types, and cps style to have a nice
type - number visual correspondance. For practice (and with
difficulty ...), I implemented a version with polymorphic variants,
but no cps (yet) :

module Dim : sig 
  type 'a dec

  val dec : [`U] dec
  val to_int : 'a dec -> int

  type 'a digit = 
    [`D0 of 'a | `D1 of 'a | `D2 of 'a | `D3 of 'a | `D4 of 'a |
     `D5 of 'a | `D6 of 'a | `D7 of 'a | `D8 of 'a | `D9 of 'a ]

  val d0 : ([< 'a digit ] as 'd) dec -> [`D0 of 'd] dec
  val d1 : 'a dec -> [`D1 of 'a] dec
  val d2 : 'a dec -> [`D2 of 'a] dec
  val d3 : 'a dec -> [`D3 of 'a] dec
  val d4 : 'a dec -> [`D4 of 'a] dec
  val d5 : 'a dec -> [`D5 of 'a] dec
  val d6 : 'a dec -> [`D6 of 'a] dec
  val d7 : 'a dec -> [`D7 of 'a] dec
  val d8 : 'a dec -> [`D8 of 'a] dec
  val d9 : 'a dec -> [`D9 of 'a] dec
end = 
struct
  type 'a digit =
    [ `D0 of 'a | `D1 of 'a | `D2 of 'a | `D3 of 'a | `D4 of 'a 
    | `D5 of 'a | `D6 of 'a | `D7 of 'a | `D8 of 'a | `D9 of
'a ]
  type 'a dec = int

  let dec = 0
  let to_int x = x

  let mkd n = fun d -> d * 10 + n
  let d0, d1, d2, d3, d4, d5, d6, d7, d8, d9 =
    mkd 0, mkd 1, mkd 2, mkd 3, mkd 4, mkd 5, mkd 6, mkd 7, mkd 8, mkd 9
end

Then,

# open Dim;;
# let x120 = (d0 (d2 (d1 dec)));;
val x120 : [ `D0 of [ `D2 of [ `D1 of [ `U]]]] Dim.dec = <abstr>
# to_int x120;;
- : int = 120
# let x32 = (d2 (d3 dec));;
val x32 : [ `D2 of [ `D3 of [ `U]]] Dim.dec = <abstr>
# x120 = x32;;
         ^^^
This expression has type [ `D2 of [ `D3 of [ `U]]] Dim.dec
but is here used with type [ `D0 of [ `D2 of [ `D1 of [ `U]]]] Dim.dec

... type error :)
As you can see the number the type encodes is reversed ('cause lack of
cps).

Now it seems to me that it's a little more expressive this way.
For example, we can define a function that will only accept numbers
(or work on array size or list size) greater than zero :

# let f_nz (x:[< 'a digit ] dec) = to_int x;;
val f_nz : [< 'a Dim.digit] Dim.dec -> int = <fun>
# let x0 = dec and x1 = (d1 dec);;
val x0 : [ `U] Dim.dec = <abstr>
val x1 : [ `D1 of [ `U]] Dim.dec = <abstr>
# f_nz x1;;
- : int = 1
# f_nz x32;;
- : int = 32
# f_nz x0;;
       ^^
This expression has type [ `U] Dim.dec but is here used with type
  ([< 'b Dim.digit] as 'a) Dim.dec
Type [ `U] is not compatible with type
  'a =
    [< `D0 of 'b
     | `D1 of 'b
     | `D2 of 'b
     | `D3 of 'b
     | `D4 of 'b
     | `D5 of 'b
     | `D6 of 'b
     | `D7 of 'b
     | `D8 of 'b
     | `D9 of 'b] 

... type error again :)
But we can go further, and allow f to work only with numbers greater than
or equal to 5 for example :

# type 'a atleast5 = [ `D5 of 'a | `D6 of 'a | `D7 of 'a | `D8 of 'a | `D9
of 'a ]
and 'a atmost4 = [`D0 of 'a | `D1 of 'a | `D2 of 'a | `D3 of 'a | `D4 of
'a ];;
*identical signature skipped*
# let f_atleast5 (x:[< 
		  | [< 'a digit ] atmost4 
		  | [< `U | 'a digit ] atleast5 
		  ] dec) = to_int x
*big type annotation skipped*
# f_atleast5 x32;;
- : int = 32
# f_atleast5 x120;;
- : int = 120
# f_atleast5 x1;;
Toplevel input:
# f_atleast5 x1;;
             ^^
This expression has type [ `D1 of [ `U]] Dim.dec but is here used with
type
  [< `D1 of [< 'b Dim.digit] as 'a] Dim.dec
*rest of big type error skipped*

... type error again, yeah :)
The idea is to encode (in the function signature) some kind of
deterministic finite automaton from the last digit of the number, which
decides if the type is valid (= if the number is in the desired
range). You can read the type of f_atleast5 as :
- let n be the number encoded in the type of x
- if the last digit of n is <= 4, then n must be at least 2 digits long (=
we don't allow the unit `U to terminate the type) to be >= 5
- if the last digit is >= 5, n is >= 5 (= we allow anything to terminate
the type)

For fun, lets work with a parameter statically known to encode a number
greater than 25 :
# type 'a atleast2 =
    [ `D2 of 'a | `D3 of 'a | `D4 of 'a 
    | `D5 of 'a | `D6 of 'a | `D7 of 'a | `D8 of 'a | `D9 of 'a ]
  and 'a atleast3 =
    [ `D3 of 'a | `D4 of 'a 
    | `D5 of 'a | `D6 of 'a | `D7 of 'a | `D8 of 'a | `D9 of 'a ]
   and 'a atmost2 = [`D0 of 'a | `D1 of 'a | `D2 of 'a ]
   and 'a atmost1 = [`D0 of 'a | `D1 of 'a ];;
*identical signature skipped*
# let f_atleast25 
    (x:[< 
       | [< [< 'a digit] atmost2 | [< `U | 'b digit ] atleast3 ] atmost4
       | [< [< 'a digit] atmost1 | [< `U | 'b digit ] atleast2 ] atleast5
       ] dec) = to_int x;;
*very big type annotation skipped*
# f_atleast25 x32;;
- : int = 32
# f_atleast25 x120;;
- : int = 120
# f_atleast25 x1;;
              ^^
This expression has type [ `D1 of [ `U]] Dim.dec but is here used with
type *very big type skipped*

Again, the type of f_atleast25 may be read :
- let n be the number encoded in the type of x, 
  with last digits XYZ (that is n >= X * 100 + Y * 10 + Z). Y and Z
  must exist but X may not exist.
- if Z <= 4 then
  - if Y <= 2 then X exists <-> n >= 25
  - if Y >= 3 then true <-> n >= 25
- if Z >= 5 then
  - if Y <= 1 then X exists <-> n >= 25
  - if Y >= 2 then true <-> n >= 25
In the same way we can encode that n should be less than something,
or between something and another, or any finite disjunction and 
conjunction of intervals as the language of DFA is closed under those
operations.
The function f_atleast120_andlessthan246 is of course left as an exercice
to the masochist reader :)

Now the questions to the courageous people that are still here :
I think the function f_atleast5 and f_atleast25 are impossible
to express with the previous solution wich involved 10 different
abstract types in Dim signature, am i right ?
When I concatenate all the Ocaml code I gave (except the 
direct calls to the f_* ) in a single file
and I compile, it's fine. But when I add :

# let _ = f_atleast5 x32 
I get :
The type of this expression, [ `D2 of [ `D3 of [ `U]]] Dim.dec,
contains type variables that cannot be generalized

Can someone explain this ?

Thanks for your attention :) ,
Ocaml really is a wonderful programming language.

Bye,
Nadji

PS: If you think my mail was off-topic let me know so I won't bother you
...
PPS: Lots of people have some very nice tricks with typing, maybe
it would be a good thing to add a section somewhere in the FAQ or the doc
for those "typing pearls". These can be very useful to get an intuition
of the limits of static typing. For example, some people posted very nice
things
about dynamic typing trick (Daniel De Rauglaude I think), memo class for
objects (Jacques Garrigue I think), of course Xavier Leroy has a bunch
of them etc ...
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners