wrapping parameterized types

wrapping parameterized types

[Christopher L Conway]

I recently ran across a rather surprising behavior in the OCaml type
system. I hope somebody may be able to advise me how to work around it
(or at least explain to me why things are the way they are!).

Suppose I want to pass around a restricted, un-parameterized list type:

# type mylist = Intlist of int list | Strlist of string list ;;
type mylist = Intlist of int list | Strlist of string list

Now I end up doing a lot of tedious case splits, like:

# let length_of_mylist = function Intlist x -> List.length x | Strlist
x -> List.length x ;;
val length_of_mylist : mylist -> int = <fun>

What one would like is something like "app_to_mylist : ('a list -> 'b)
-> mylist -> 'b" so one could write "app_to_mylist List.length", but:

# let app_to_mylist f = function Intlist x -> f x | Strlist x -> f x ;;
Characters 65-66:
  let app_to_mylist f = function Intlist x -> f x | Strlist x -> f x ;;
                                                                   ^
This expression has type string list but is here used with type int list

The solution I've tripped over is to pass in separate functions for
the different cases, and then (only somewhat less tediously than
above) duplicate the same function at the call site:

# let app_to_mylist (fi,fs) = function Intlist x -> fi x | Strlist x -> fs x ;;
val app_to_mylist : (int list -> 'a) * (string list -> 'a) -> mylist -> 'a =
  <fun>
# let length_of_mylist = app_to_mylist (List.length, List.length);;
val length_of_mylist : mylist -> int = <fun>

I can't help but feel there is a more elegant way to handle this,
perhaps drawing in objects or functors. Any suggestions?

This question arises from an attempt to use the APRON library, which
provides types parameterized by numerical domain, alongside other
numerical tools in a uniform way---the APRON interface deals with the
parameterized types generically, but I need to hoist the abstraction
up one layer and deal with both APRON and non-APRON types generically.
The details are far too ugly to wade into here...

Thanks,
Chris

Re: [Caml-list] wrapping parameterized types

[Chris King]

On 5/3/07, Christopher L Conway <cconway@cs.nyu.edu> wrote:
> # let app_to_mylist f = function Intlist x -> f x | Strlist x -> f x ;;
> Characters 65-66:
>   let app_to_mylist f = function Intlist x -> f x | Strlist x -> f x ;;
>                                                                    ^
> This expression has type string list but is here used with type int list

The problem is, when O'Caml tries to infer the type of f, it
arbitrarily chooses string list -> 'a and dies when it finds it
applied to an int list.  And although the type you want is 'a list ->
'b, O'Caml certainly won't infer this, since you'd have polymorphic
functions like that popping up every time you made a type mistake
(this is the same reason why non-homogenous lists of objects aren't
automatically coerced to a union of their types).

So you might expect that the following would work:

let app_to_mylist (f: 'a list -> 'b) = function Intlist x -> f x |
Strlist x -> f x ;;

but this doesn't force O'Caml to do anything, it's still free to
refine 'a to int or string.  (Just like how if you write "let x: 'a =
5", x is still an int).

The solution is to use existential types.  In a record, you can tell
O'Caml that a particular function _must_ be polymorphic:

type 'b mylistfun = { listfun: 'a. 'a list -> 'b }

Prefixing f's type with "'a." tells O'Caml that 'a is an existential
type variable, meaning that f must be able to work with any 'a.  Note
that 'a doesn't appear in mylistfun's list of type variables (since it
would make no sense to choose a type for 'a).

So armed with mylistfun, you can rewrite app_to_mylist as:

# let app_to_mylist { listfun = f } = function Intlist x -> f x |
Strlist x -> f x;;
val app_to_mylist : 'a mylistfun -> mylist -> 'a = <fun>

and all is well:

#  app_to_mylist { listfun = List.length } (Intlist [1;2;3]);;
- : int = 3

Unfortunately this trick only works with records and objects, so
you're forced to box up the function before handing it to
app_to_mylist.  (I forget the reason why you can't do this in general
but I'm sure someone else can enlighten us both.)

Hope this helps.

- Chris

Re: [Caml-list] wrapping parameterized types

[skaller]

On Thu, 2007-05-03 at 19:16 -0400, Chris King wrote:
> On 5/3/07, Christopher L Conway <cconway@cs.nyu.edu> wrote:

> The solution is to use existential types.  In a record, you can tell
> O'Caml that a particular function _must_ be polymorphic:
> 
> type 'b mylistfun = { listfun: 'a. 'a list -> 'b }

I'm still confused why this is called an existential, when
clearly the quantification is universal.



-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net

Re: [Caml-list] wrapping parameterized types

[Dirk Thierbach]

On Fri, May 04, 2007 at 11:10:03AM +1000, skaller wrote:
> On Thu, 2007-05-03 at 19:16 -0400, Chris King wrote:
> > On 5/3/07, Christopher L Conway <cconway@cs.nyu.edu> wrote:

> > The solution is to use existential types.  In a record, you can tell
> > O'Caml that a particular function _must_ be polymorphic:
> > 
> > type 'b mylistfun = { listfun: 'a. 'a list -> 'b }

> I'm still confused why this is called an existential, when
> clearly the quantification is universal.

It's because the universal quantifier is in a "negative" position,
which is equivalent to an existential quantifier on the outside.
Just pretend they are logic formulae instead of types, and then

(\forall a. a) -> b   is equivalent to   \exists a. (a -> b)

using DeMorgan's rule.

- Dirk

Re: [Caml-list] wrapping parameterized types

[rossberg]

"skaller" <skaller@users.sourceforge.net> wrote:
> On Thu, 2007-05-03 at 19:16 -0400, Chris King wrote:
>> The solution is to use existential types.  In a record, you can tell
>> O'Caml that a particular function _must_ be polymorphic:
>>
>> type 'b mylistfun = { listfun: 'a. 'a list -> 'b }
>
> I'm still confused why this is called an existential, when
> clearly the quantification is universal.

You have reason to be confused, because this is no existential type.

Dirk Thierbach:
>It's because the universal quantifier is in a "negative" position,
>which is equivalent to an existential quantifier on the outside.
>Just pretend they are logic formulae instead of types, and then
>
>(\forall a. a) -> b   is equivalent to   \exists a. (a -> b)

Actually, no, these are not equivalent. Only the following are:

(\exists a. a) -> b   is equivalent to   \forall a. (a -> b)

Here is the constructive proof. Assume:

  f : (exists a.a) -> b
  g : forall a. (a -> b)

You can construct g from f and vice versa:

  g = \a. \a:x. f <a,x>
  f = \y:(exists a.a). let <a,x> = y in g a x

Cheers,
- Andreas

Re: [Caml-list] wrapping parameterized types

[Andrej Bauer]

rossberg@ps.uni-sb.de wrote:
> "skaller" <skaller@users.sourceforge.net> wrote:
>> On Thu, 2007-05-03 at 19:16 -0400, Chris King wrote:
>>> The solution is to use existential types.  In a record, you can tell
>>> O'Caml that a particular function _must_ be polymorphic:
>>>
>>> type 'b mylistfun = { listfun: 'a. 'a list -> 'b }
>> I'm still confused why this is called an existential, when
>> clearly the quantification is universal.
> 
> You have reason to be confused, because this is no existential type.
> 
> Dirk Thierbach:
>> It's because the universal quantifier is in a "negative" position,
>> which is equivalent to an existential quantifier on the outside.
>> Just pretend they are logic formulae instead of types, and then
>>
>> (\forall a. a) -> b   is equivalent to   \exists a. (a -> b)
> 
> Actually, no, these are not equivalent. Only the following are:
> 
> (\exists a. a) -> b   is equivalent to   \forall a. (a -> b)

Right, and this is in accordance with the terminology. Note that Dirk
misread the precedence of operators: in ocaml

  'a . 'a list -> 'b

means

  'a . ('a list -> 'b)

and not ('a . 'a list) -> 'b. So everything is fine. I do agree with
skaller that it is a bit perverse to call a quantifier "existential"
when it is obviously the universal quantifier, even if it is equivalent
to a formula containing an existential.

Andrej

Re: [Caml-list] wrapping parameterized types

[Dirk Thierbach]

Andrej Bauer wrote:
>rossberg@ps.uni-sb.de wrote:

>> Dirk Thierbach:
>>> It's because the universal quantifier is in a "negative" position,
>>> which is equivalent to an existential quantifier on the outside.
>>> Just pretend they are logic formulae instead of types, and then
>>>
>>> (\forall a. a) -> b   is equivalent to   \exists a. (a -> b)
>> 
>> Actually, no, these are not equivalent. 

Well, as classical logical formulae, they clearly are :-) Which IMHO
is enough to explain the name. Notice I said "pretend", and didn't use
the word "intuitionistically".

>> Only the following are:
>> 
>> (\exists a. a) -> b   is equivalent to   \forall a. (a -> b)

But that doesn't explain why the usage in the example is called
"existential". All "normal" types are forall-quantified on the outside,
so this isn't really a new feature in any way.

> Right, and this is in accordance with the terminology. 

Well, then maybe I don't understand the terminology :-)

> Note that Dirk misread the precedence of operators:

No, I didn't, but maybe I was to terse. The point is that records
in OCaml allow rank-2 polymorphism, and one can use rank-2 polymorphism
to encode existential types. The crucial point in the example is here:

>>>> type 'b mylistfun = { listfun: 'a. 'a list -> 'b }
[...]
>>>> val app_to_mylist : 'a mylistfun -> mylist -> 'a = <fun>

So, ignoring records, app_to_mylist has the type

app_to_mylist : (\forall 'a. 'a list -> 'b) -> mylist -> 'b

Now, "morally" this is similar to

app_to_mylist : \exists 'a. ('a list -> 'b) -> mylist -> 'b

as pointed out before.  So one can indeed pretend that 'a is
existentially qualified in this function. And this is important,
because that's what makes the whole thing work ("there is a type 'a
such that app_to_mylist executes, but we don't now in advance which
one"). And the encoding of "real" existential types using rank-2
polymorphisms is very similar. Which is again a reason to make a
connection between existential quantifiers and forall-quantifiers in
negative positions, and call such an encoding "existential type".

OTOH, the conversion from (\forall 'a. 'a list -> 'b) to
((\exists 'a. 'a list) -> b) really doesn't explain anything. Or maybe
it does, and I don't understand it, but so far, the other explanation
makes a lot more sense to me.

- Dirk

Re: [Caml-list] wrapping parameterized types

[Christopher L Conway]

Can anyone point me to where the semantics of these, um, existential
type declarations are defined? This topic is mentioned only scantly in
the manual. I'd also be interested in pointers to the underlying type
theory.

Thanks,
Chris

On 5/4/07, Dirk Thierbach <dthierbach@gmx.de> wrote:
> Andrej Bauer wrote:
> >rossberg@ps.uni-sb.de wrote:
>
> >> Dirk Thierbach:
> >>> It's because the universal quantifier is in a "negative" position,
> >>> which is equivalent to an existential quantifier on the outside.
> >>> Just pretend they are logic formulae instead of types, and then
> >>>
> >>> (\forall a. a) -> b   is equivalent to   \exists a. (a -> b)
> >>
> >> Actually, no, these are not equivalent.
>
> Well, as classical logical formulae, they clearly are :-) Which IMHO
> is enough to explain the name. Notice I said "pretend", and didn't use
> the word "intuitionistically".
>
> >> Only the following are:
> >>
> >> (\exists a. a) -> b   is equivalent to   \forall a. (a -> b)
>
> But that doesn't explain why the usage in the example is called
> "existential". All "normal" types are forall-quantified on the outside,
> so this isn't really a new feature in any way.
>
> > Right, and this is in accordance with the terminology.
>
> Well, then maybe I don't understand the terminology :-)
>
> > Note that Dirk misread the precedence of operators:
>
> No, I didn't, but maybe I was to terse. The point is that records
> in OCaml allow rank-2 polymorphism, and one can use rank-2 polymorphism
> to encode existential types. The crucial point in the example is here:
>
> >>>> type 'b mylistfun = { listfun: 'a. 'a list -> 'b }
> [...]
> >>>> val app_to_mylist : 'a mylistfun -> mylist -> 'a = <fun>
>
> So, ignoring records, app_to_mylist has the type
>
> app_to_mylist : (\forall 'a. 'a list -> 'b) -> mylist -> 'b
>
> Now, "morally" this is similar to
>
> app_to_mylist : \exists 'a. ('a list -> 'b) -> mylist -> 'b
>
> as pointed out before.  So one can indeed pretend that 'a is
> existentially qualified in this function. And this is important,
> because that's what makes the whole thing work ("there is a type 'a
> such that app_to_mylist executes, but we don't now in advance which
> one"). And the encoding of "real" existential types using rank-2
> polymorphisms is very similar. Which is again a reason to make a
> connection between existential quantifiers and forall-quantifiers in
> negative positions, and call such an encoding "existential type".
>
> OTOH, the conversion from (\forall 'a. 'a list -> 'b) to
> ((\exists 'a. 'a list) -> b) really doesn't explain anything. Or maybe
> it does, and I don't understand it, but so far, the other explanation
> makes a lot more sense to me.
>
> - Dirk
>
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>
>

Re: [Caml-list] wrapping parameterized types

[Christopher L Conway]

Chris,

Thanks! This works! There's one tiny little bug in your suggestion. It
should be:

let app_to_mylist f = function Intlist x -> f.listfun x | Strlist x ->
f.listfun x;;

Using pattern matching on the function argument leads right back to
the original type instantiation problem.

Regards,
Chris

On 5/3/07, Chris King <colanderman@gmail.com> wrote:
> On 5/3/07, Christopher L Conway <cconway@cs.nyu.edu> wrote:
> > # let app_to_mylist f = function Intlist x -> f x | Strlist x -> f x ;;
> > Characters 65-66:
> >   let app_to_mylist f = function Intlist x -> f x | Strlist x -> f x ;;
> >                                                                    ^
> > This expression has type string list but is here used with type int list
>
> The problem is, when O'Caml tries to infer the type of f, it
> arbitrarily chooses string list -> 'a and dies when it finds it
> applied to an int list.  And although the type you want is 'a list ->
> 'b, O'Caml certainly won't infer this, since you'd have polymorphic
> functions like that popping up every time you made a type mistake
> (this is the same reason why non-homogenous lists of objects aren't
> automatically coerced to a union of their types).
>
> So you might expect that the following would work:
>
> let app_to_mylist (f: 'a list -> 'b) = function Intlist x -> f x |
> Strlist x -> f x ;;
>
> but this doesn't force O'Caml to do anything, it's still free to
> refine 'a to int or string.  (Just like how if you write "let x: 'a =
> 5", x is still an int).
>
> The solution is to use existential types.  In a record, you can tell
> O'Caml that a particular function _must_ be polymorphic:
>
> type 'b mylistfun = { listfun: 'a. 'a list -> 'b }
>
> Prefixing f's type with "'a." tells O'Caml that 'a is an existential
> type variable, meaning that f must be able to work with any 'a.  Note
> that 'a doesn't appear in mylistfun's list of type variables (since it
> would make no sense to choose a type for 'a).
>
> So armed with mylistfun, you can rewrite app_to_mylist as:
>
> # let app_to_mylist { listfun = f } = function Intlist x -> f x |
> Strlist x -> f x;;
> val app_to_mylist : 'a mylistfun -> mylist -> 'a = <fun>
>
> and all is well:
>
> #  app_to_mylist { listfun = List.length } (Intlist [1;2;3]);;
> - : int = 3
>
> Unfortunately this trick only works with records and objects, so
> you're forced to box up the function before handing it to
> app_to_mylist.  (I forget the reason why you can't do this in general
> but I'm sure someone else can enlighten us both.)
>
> Hope this helps.
>
> - Chris
>
>