[Caml-list] Polymorphic Variants and Number Parameterized Types

[Caml-list] Polymorphic Variants and Number Parameterized Types

[Nadji.Gauthier]

*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

Re: [Caml-list] Polymorphic Variants and Number Parameterized Types

[John Max Skaller]

Nadji.Gauthier@lip6.fr wrote:

>*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*
>
There is one importance of such demonstrations: they act as a proof
that adding integer constants to the static type systems is
'safe and sound'.

 Of course, C++ is ahead here, it already admits generics parameterised
by both types and integers ..  <Ducks for cover ... >

-- 
John Max Skaller, mailto:skaller@ozemail.com.au
snail:10/1 Toxteth Rd, Glebe, NSW 2037, Australia.
voice:61-2-9660-0850




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

Re: [Caml-list] Polymorphic Variants and Number Parameterized Types

[Brian Rogoff]

On Sat, 27 Apr 2002, John Max Skaller wrote:
> Nadji.Gauthier@lip6.fr wrote:
>
> >*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*

Nice tricks Nadji! I didn't have time to try out everything you showed,
but I think that trick is more powerful than the other one, which doesn't
use variants. Also, I'm willing to bet that you uncovered a bug in the
type checker (with the "variables can't be generalized" only when in
the compiler). Have you filed a bug report yet?

> There is one importance of such demonstrations: they act as a proof
> that adding integer constants to the static type systems is
> 'safe and sound'.

I think if you're going to take the conclusion that all of these tricks
are worthwhile, you'll want a language with dependent types. In the
general case, you may get undecidable typing (like Cayenne, which is
very very cool) but there are also restricted systems like Xi's DeCaml
which may be useful.

>  Of course, C++ is ahead here, it already admits generics parameterised
> by both types and integers ..  <Ducks for cover ... >

It could be useful when modeling electronic components to have the
bitwidth of a component as part of a type, and to be able to say stuff
in the type system about how that width changes as we build components.
There was a neat posting in c.l.f. recently about such a trick using
(non-"standard" features of) Haskell.

I don't think C++ or Ada generics (which also parameterize over values)
help you much there. Besides, ML uses the module system to parameterize
over values.

-- Brian
-------------------
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

Re: [Caml-list] Polymorphic Variants and Number Parameterized Types

[John Max Skaller]

Brian Rogoff wrote:

>> Of course, C++ is ahead here, it already admits generics parameterised
>>by both types and integers ..  <Ducks for cover ... >
>>
>
>I don't think C++ or Ada generics (which also parameterize over values)
>help you much there. Besides, ML uses the module system to parameterize
>over values.
>
Yeah, you're right.  Although, there aren't many types that can use that 
information.
(No fixed lenth arrays for example).

Hmmm... beginnners question on module system .. can you recurse on it?
I'm guessing not, since there are neither specialisations nor overloading,
there's be no way to stop the recursion. ..??

[In C++, you can recurse on an integer parameter, using a 
specialisation/overload
to terminate the recursion... its a turing complete functional programming
language .. slightly messy though :]

-- 
John Max Skaller, mailto:skaller@ozemail.com.au
snail:10/1 Toxteth Rd, Glebe, NSW 2037, Australia.
voice:61-2-9660-0850




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

Re: [Caml-list] Polymorphic Variants and Number Parameterized Types

[Nadji.Gauthier]

> use variants. Also, I'm willing to bet that you uncovered a bug in the   
> type checker (with the "variables can't be generalized" only when in     
> the compiler). Have you filed a bug report yet?

I haven't. And since I don't fully understand PV typing,
I prefer not to bother the developers (I fear the
"this is a feature not a bug" reply :))
But I understand that there may be error when source
is compiled when there aren't in the interpreter, ex:
  let x = ref []
When compiled, this gives :
  The type of this expression, '_a list ref,
  contains type variables that cannot be generalized
And this is perfectly fair (think of 2 different modules
accessing x, there may be a type clash).
I think the same thing happenned
in my previous mail but I haven't managed to isolate the problem yet.

Nadji
-------------------
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

Re: [Caml-list] Polymorphic Variants and Number Parameterized Types

[Brian Rogoff]

On Mon, 29 Apr 2002 Nadji.Gauthier@lip6.fr wrote:
> > use variants. Also, I'm willing to bet that you uncovered a bug in the
> > type checker (with the "variables can't be generalized" only when in
> > the compiler). Have you filed a bug report yet?
>
> I haven't. And since I don't fully understand PV typing,
> I prefer not to bother the developers (I fear the
> "this is a feature not a bug" reply :))

Sure, but it is also possible you found a problem and we all could benefit
from its removal.

> But I understand that there may be error when source
> is compiled when there aren't in the interpreter, ex:
>   let x = ref []
> When compiled, this gives :
>   The type of this expression, '_a list ref,
>   contains type variables that cannot be generalized
> And this is perfectly fair (think of 2 different modules
> accessing x, there may be a type clash).

That's right.

> I think the same thing happenned
> in my previous mail but I haven't managed to isolate the problem yet.

I played a bit with your example, and while I haven't isolated the
problem, I found that there is no problem with the reported expression.
The problem only happened when the f_ngt5 (or whatever you called it)
was included and disappeared when it was removed. So it seems like a
genuine bug.

-- Brian
-------------------
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

Re: [Caml-list] Polymorphic Variants and Number Parameterized Types

[Francois Pottier]

Hi Andreas,

On Mon, Apr 29, 2002 at 06:48:11PM +0200, Andreas Rossberg wrote:
> 
> Well, if you have a functor like
> 
> 	F : functor(X : sig module type S  module Y:S end) -> ...
> 
> then it would be polymorphic in an unknown number of types.

Perhaps our views differ. What I gathered from Jones' and Russo's
papers was that modules do not contain types. So, the module type
S cannot be a component of X; rather, the type of the functor F
will be universally quantified over S. This leads me to something
like:

  F : forall S. functor (X : S) -> ...

where the distinction between X and Y is eliminated, because it
becomes superfluous. In fact, the `functor' syntax and the name
X are just sugar, since a functor is a function. So I would really
write

  F : forall S. S -> ...

> The application
> 
> 	F (struct module type S = sig type t type u val x : t end 
> 	          module Y = struct type t = int
> 	                            type u = bool
> 	                            val x = 7 end
> 	   end)
> 
> corresponds to something like
> 
> 	F {t:*,u:*} {x:int} {t=int,u=bool} {Y={x=7}}

I would simply apply

  F { x : int } { x = 7 }

or, perhaps (if abstraction is desired)

  F (exists t,u.{ x : t }) (pack { x = 7 } as exists t,u.{ x : t })

So, in this example, we seem to need neither higher kinds nor
kind polymorphism. But perhaps my encoding doesn't have the
features you'd wish?

-- 
François Pottier
Francois.Pottier@inria.fr
http://pauillac.inria.fr/~fpottier/
-------------------
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

Re: [Caml-list] Polymorphic Variants and Number Parameterized Types

[Andreas Rossberg]

Hi François,

> > Note that Russo showed [1] that you can actually get rid of dependent
> > typing and interpret ML modules (without nested signatures) as a lambda
> > calculus with higher-order polymorphism (i.e., definitely not
> > simply-typed). The basic idea is to view functors as functions
> > polymorphic over their type arguments.
> 
> This interesting idea was also developed by Mark Jones:

IIRC, he does not consider generative functors, though.

> > In this setting, adding abstract signatures would at least require adding
> > polymorphic kinds, I believe.
> 
> What do you mean? In this encoding, modules are only records, so module types
> are ordinary types, and there is no distinction between ordinary abstract
> types (introduced by explicit polymorphic abstraction) and ``abstract
> signatures''. There is, as far as I can tell, no need for kind polymorphism.

Well, if you have a functor like

	F : functor(X : sig module type S  module Y:S end) -> ...

then it would be polymorphic in an unknown number of types. To capture
this, you had to make the functor polymorphic in the kind carrying the
record of abstract types bound in S (i.e. you would also need record
kinds). Something along the lines of:

	F : forall k. forall S:*. forall ts:k. {Y:S} -> ...

The application

	F (struct module type S = sig type t type u val x : t end 
	          module Y = struct type t = int
	                            type u = bool
	                            val x = 7 end
	   end)

corresponds to something like

	F {t:*,u:*} {x:int} {t=int,u=bool} {Y={x=7}}

I'm being sketchy here, of course, since I haven't thought about it in
real depth. It probably gets even messier when you go higher-order:
consider signatures projected from an applicative functor, for example.
In that case you might even need quantifiers on the kind level to encode
it. Also, the kind k should be restricted to record kinds, so you want
some subkinding discipline (or row polymorphism on the kind level? ;-).

Well, and somewhere in that mess we must have taken the step into the
realms of undecidable subtyping (because if it encodes OCaml modules it
must be undecidable).

Cheers,

	- Andreas
-- 
Andreas Rossberg, rossberg@ps.uni-sb.de

"Computer games don't affect kids; I mean if Pac Man affected us
 as kids, we would all be running around in darkened rooms, munching
 magic pills, and listening to repetitive electronic music."
 - Kristian Wilson, Nintendo Inc.
-------------------
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

Re: [Caml-list] Polymorphic Variants and Number Parameterized Types

[Francois Pottier]

Hi,

> Note that Russo showed [1] that you can actually get rid of dependent
> typing and interpret ML modules (without nested signatures) as a lambda
> calculus with higher-order polymorphism (i.e., definitely not
> simply-typed). The basic idea is to view functors as functions
> polymorphic over their type arguments.

This interesting idea was also developed by Mark Jones:

  @InProceedings{jones-96,
    author       = "Mark P. Jones",
    title        = "Using Parameterized Signatures to Express Modular
		   Structure",
    booktitle    = "Proceedings of the 23rd {ACM} Symposium on Principles
		   of Programming Languages",
    publisher    = "ACM Press",
    month        = jan,
    year         = "1996",
    address      = "St. Petersburg Beach, Florida",
    note         = "\url{http://www.cse.ogi.edu/~mpj/pubs/paramsig.html}",
  }

as well as (in a couple of much more technical papers) by Zhong Shao.

> In this setting, adding abstract signatures would at least require adding
> polymorphic kinds, I believe.

What do you mean? In this encoding, modules are only records, so module types
are ordinary types, and there is no distinction between ordinary abstract
types (introduced by explicit polymorphic abstraction) and ``abstract
signatures''. There is, as far as I can tell, no need for kind polymorphism.

-- 
François Pottier
Francois.Pottier@inria.fr
http://pauillac.inria.fr/~fpottier/
-------------------
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

Re: [Caml-list] Polymorphic Variants and Number Parameterized Types

[Andreas Rossberg]

"Krishnaswami, Neel" wrote:
> 
> Pascal Cuoq [mailto:pascal.cuoq@inria.fr] wrote:
> > Neel Krishnaswami wrote:
> >
> > > There's no recursion in the module system because that would break
> > > the termination guarantee. If you think of modules as records, and
> > > functors as lambda abstractions, you can see that the module system
> > > defines a simply-typed lambda calculus. As you've noticed with C++,
> > > adding recursion to it would mean you can write nonterminating module
> > > expressions. (All this is wonderfully clearly explained in
> > > the paper, "A modular  module system".)
> >
> > I'm not sure about "simply-typed". Did the situation change since
> > that of http://caml.inria.fr/archives/199907/msg00027.html ?
> 
> Wow! I didn't even know that was possible. I thought that typechecking
> record subtyping was decidable...?

Well, module types are (a limited form of) dependent types. What
concretely triggers undecidability of subtyping in OCaml is the presence
of abstract module types, at least in combination with the
contravariance of higher-order functors.

Note that Russo showed [1] that you can actually get rid of dependent
typing and interpret ML modules (without nested signatures) as a lambda
calculus with higher-order polymorphism (i.e., definitely not
simply-typed). The basic idea is to view functors as functions
polymorphic over their type arguments. In this setting, adding abstract
signatures would at least require adding polymorphic kinds, I believe.

[1]

@inproceedings{Russo:NonDependentTypes,
  author	= "Claudio Russo",
  title		= "Non-Dependent Types for {Standard} {ML} Modules",
  booktitle	= "International Conference on Principles and
                   Practice of Declarative Programming",
  address	= "Paris, France",
  year		= 1999,
  month		= sep,
}

-- 
Andreas Rossberg, rossberg@ps.uni-sb.de

"Computer games don't affect kids; I mean if Pac Man affected us
 as kids, we would all be running around in darkened rooms, munching
 magic pills, and listening to repetitive electronic music."
 - Kristian Wilson, Nintendo Inc.
-------------------
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