Polymorphic Variants

Polymorphic Variants

[Tom]

[-- Attachment #1: Type: text/plain, Size: 568 bytes --]

I have a question... I hope it will not be dismissed right away, thou I
guess most of you will find it stupid (some might however agree with me...
hopefully).

Cut the crap!

So... why actually are polymorphic variants useful? Why can't they simply be
implemented as normal, concrete (or how would you call them? ...) variants?
Doesn't the use of polymorphic variants just mess up the function type?

I'm not orthogonally against polymorphic variants, it's just that I am
looking for an alternative concept that could be used instead... Maybe
subtyped records?

- Tom

[-- Attachment #2: Type: text/html, Size: 614 bytes --]

Re: [Caml-list] Polymorphic Variants

[Seth J. Fogarty]

I find them prinicipally useful in three situations:

1) When I am writing code for an easy subset of a problem, and wish to
extend it later. This is the least useful case, easiest to replace.

2) When I have different overlapping kinds of data, with a common root
and common parent, and functions that are only defined on certain
branches of the 'type tree.' This would be the hardest to replicate.

3) When I have intermediate labelled data for gathering different
subproblems together. This is the neatest use: I extend my algorithm
to handle a case that might return the top two, and I just add an
additional case to the destructor for `TopTwo instead of `Best or
`SecondBest.

On 1/16/07, Tom <tom.primozic@gmail.com> wrote:
> I have a question... I hope it will not be dismissed right away, thou I
> guess most of you will find it stupid (some might however agree with me...
> hopefully).
>
> Cut the crap!
>
> So... why actually are polymorphic variants useful? Why can't they simply be
> implemented as normal, concrete (or how would you call them? ...) variants?
> Doesn't the use of polymorphic variants just mess up the function type?
>
> I'm not orthogonally against polymorphic variants, it's just that I am
> looking for an alternative concept that could be used instead... Maybe
> subtyped records?
>
> - Tom
>
> _______________________________________________
> 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
>
>
>


-- 
Seth Fogarty             sfogarty@[gmail.com|rice.edu|livejournal]
Neep-neep at large    AIM: Sorrath
"Let us not seek to satisfy our thirst for freedom by drinking from
the cup of bitterness and hatred." - Martin Luther King, Jr.

Re: [Caml-list] Polymorphic Variants

[Tom]

[-- Attachment #1: Type: text/plain, Size: 840 bytes --]

On 16/01/07, Seth J. Fogarty <sfogarty@gmail.com> wrote:
>
>
> 2) When I have different overlapping kinds of data, with a common root
> and common parent, and functions that are only defined on certain
> branches of the 'type tree.' This would be the hardest to replicate.
>

Could this be replicated by either
using overloaded non-polymorphic variants, meaning that say Int of int can
be shared by many types (almost like polymorphic variants, just that it is
declared, and thus (at least I believe so) more typesafe)

using records with overloaded fields and subtyping, so that you could have:
type top = {common of string}
type one_level_deep = {top | my_only of int}

type independent = {my_only of string}
so this would be possible:
let to_str x -> x.common

to_str {common = "first"}; to_str {common = "second"; my_only = 0}
?

- Tom

[-- Attachment #2: Type: text/html, Size: 1425 bytes --]

Re: [Caml-list] Polymorphic Variants

[Seth J. Fogarty]

On 1/16/07, Tom <tom.primozic@gmail.com> wrote:
>
>
> On 16/01/07, Seth J. Fogarty <sfogarty@gmail.com> wrote:
> >
> > 2) When I have different overlapping kinds of data, with a common root
> > and common parent, and functions that are only defined on certain
> > branches of the 'type tree.' This would be the hardest to replicate.
> >
>
> Could this be replicated by either
> using overloaded non-polymorphic variants, meaning that say Int of int can
> be shared by many types (almost like polymorphic variants, just that it is
> declared, and thus (at least I believe so) more typesafe)

Are you going to allow translation between these? Rho-variable
polymorphism is 'The Right Thing To Do' in this case with minimal type
annotation.

> using records with overloaded fields and subtyping, so that you could have:
> type top = {common of string}
> type one_level_deep = {top | my_only of int}
>
> type independent = {my_only of string}
> so this would be possible:
> let to_str x -> x.common
>
> to_str {common = "first"}; to_str {common = "second"; my_only = 0}
> ?

OCaml does not, as far as I know, have any structural typing for
records.. and I am not sure this would be at all cleaner. It might
WORK, but it would be just as ugly, if not uglier.


-- 
Seth Fogarty             sfogarty@[gmail.com|rice.edu|livejournal]
Neep-neep at large    AIM: Sorrath
"Let us not seek to satisfy our thirst for freedom by drinking from
the cup of bitterness and hatred." - Martin Luther King, Jr.

Re: [Caml-list] Polymorphic Variants

[Edgar Friendly]

Seth J. Fogarty wrote:
>> using records with overloaded fields and subtyping, so that you could
>> have:
>> type top = {common of string}
>> type one_level_deep = {top | my_only of int}
>>
>> type independent = {my_only of string}
>> so this would be possible:
>> let to_str x -> x.common
>>
>> to_str {common = "first"}; to_str {common = "second"; my_only = 0}
>> ?
> 
> OCaml does not, as far as I know, have any structural typing for
> records.. and I am not sure this would be at all cleaner. It might
> WORK, but it would be just as ugly, if not uglier.
> 
> 
OCaml's records are tuples with named accessors to the components.
Within a namespace, these accessors must be unique, so the type
independent wouldn't be possible, because the my_only component wouldn't
always be in the same position.

E.

Re: [Caml-list] Polymorphic Variants

[Lukasz Stafiniak]

On 1/16/07, Seth J. Fogarty <sfogarty@gmail.com> wrote:
> On 1/16/07, Tom <tom.primozic@gmail.com> wrote:
> >
> >
> > On 16/01/07, Seth J. Fogarty <sfogarty@gmail.com> wrote:
...
> > using records with overloaded fields and subtyping, so that you could have:
> > type top = {common of string}
> > type one_level_deep = {top | my_only of int}
> >
> > type independent = {my_only of string}
> > so this would be possible:
> > let to_str x -> x.common
> >
> > to_str {common = "first"}; to_str {common = "second"; my_only = 0}
> > ?
>
> OCaml does not, as far as I know, have any structural typing for
> records.. and I am not sure this would be at all cleaner. It might
> WORK, but it would be just as ugly, if not uglier.
>
OCaml has objects, which is a heavy-weight solution to the "structural
subtyping for records" problem. Polymorphic variants make one wonder,
if such light-weight solution could exist for records also, and you
conjecture, that it doesn't. What is the minimal nice version of
structural subtyping for records? Is it objects without classes and
field / method separation (but with late binding)?

Re: [Caml-list] Polymorphic Variants

[skaller]

On Tue, 2007-01-16 at 15:23 -0600, Seth J. Fogarty wrote:

> OCaml does not, as far as I know, have any structural typing for
> records.. 

Hmm .. Felix does, and it supports subtyping (by explicit coercion).
So why doesn't Ocaml have it? Yes, it would be "yet another product
type", bringing the total to 4 in Ocaml (tuples, records, structurally
typed records and classes).

Come to think of it .. aren't classes structurally typed records?


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

Re: [Caml-list] Polymorphic Variants

[Jonathan Roewen]

There are interesting, and extremely useful use cases for polymorphic
variants. One very cool example (IMO) is an xhtml module which mixes
phantom types with polymorphic variants so that the compiler enforces
creation of valid xhtml documents (with some limitations...).

Also, OCaml has ways to control whether a polymorphic variant argument
to a function is open/extensible or not.

As for the records issue: you can wrap them in sub modules to
workaround the name clash problem by fully qualifying the fields with
their module name.

E.g.

module A = struct
  type t = { x : int; y : int }
end

module B = struct
  type t = { x : float; y : float }
end

open A;;
open B;;

let a = { A.x = 2; A.y = 3 };;
let b = { B.x = 1.; B.y = 2. };;

let x_from_A v = v.A.x;;
let x_from_B v = v.B.x;;

Jonathan

On 1/17/07, Tom <tom.primozic@gmail.com> wrote:
> I have a question... I hope it will not be dismissed right away, thou I
> guess most of you will find it stupid (some might however agree with me...
> hopefully).
>
> Cut the crap!
>
> So... why actually are polymorphic variants useful? Why can't they simply be
> implemented as normal, concrete (or how would you call them? ...) variants?
> Doesn't the use of polymorphic variants just mess up the function type?
>
> I'm not orthogonally against polymorphic variants, it's just that I am
> looking for an alternative concept that could be used instead... Maybe
> subtyped records?
>
> - Tom
>
> _______________________________________________
> 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] Polymorphic Variants

[Jacques GARRIGUE]

From: Tom <tom.primozic@gmail.com>
> So... why actually are polymorphic variants useful? Why can't they simply be
> implemented as normal, concrete (or how would you call them? ...) variants?

The original motivation was for the LablTk library, where some types
(index for instance) have lots of small variations. At that point
there where several options
* overloading (but ocaml loathes overloading, you could say that the
  total absence of overloading is essential to the language)
* refinement types: define a type with all constructors, and have
  restricted versions of it where only some constructors are allowed
* full polymorphism, i.e. polymorphic variants

If you eliminate the first option, then the choice is between
refinement types and polymorphic variants. Refinement types are rather
attractive: they combine precise typing with explicit declarations.
The arguments in favour of polymorphic variants are
* they were somehow easier to add, as they are an orthogonal extension
  of the type system
* one can add new cases afterwards.
* they are defined structurally: two identical definitions in two
  different modules are equivalent. This can be pretty handy at times.
* you don't need to open a module to use them: mixes nicely with ocaml
  programming style

>From modularity considerations, it ends up being nicer to write
     type t = [`A of int |`B of bool]
     type u = [t | `C of char]
than
     type u = A of int | B of bool | C of char
     type t = u[A B]

Afterwards I discovered that, using some idioms, they also allow
extensible programs in a very concise way. (Much more concise than
objects, when they are relevant.)

> Doesn't the use of polymorphic variants just mess up the function type?
What do you mean by "mess up the function type"?
If you mean that, without type annotations, types and errors become
very hard to read, this is true, but the manual explicitely encourages
to add type annotations :-)

> I'm not orthogonally against polymorphic variants, it's just that I am
> looking for an alternative concept that could be used instead... Maybe
> subtyped records?

In terms of expressiveness, you can simulate polymorphic variants
using objects (which are subtyped records,) but this is often much
more verbose, and requires higher order types. I have some code using
objects (visitor pattern), recursive modules, lazyness, and private
row types, in an utterly non trivial way, just to do what can be done
by standard recursive function definitions using polymorphic variants...

Jacques Garrigue

Re: [Caml-list] Polymorphic Variants

[Christophe TROESTLER]

On Wed, 17 Jan 2007, Jacques GARRIGUE <garrigue@math.nagoya-u.ac.jp> wrote:
> 
> [...] I have some code using objects (visitor pattern), recursive
> modules, lazyness, and private row types, in an utterly non trivial
> way, just to do what can be done by standard recursive function
> definitions using polymorphic variants...

Sounds like a good case to see & learn the power of polymorphic
variants in action.  Are the two codes available somewhere (if
possible with some explanations ?) or are you simply referring to your
paper "Code reuse through polymorphic variants" ?

Regards,
ChriS

Re: [Caml-list] Polymorphic Variants

[Jacques Garrigue]

From: Christophe TROESTLER <Christophe.Troestler+ocaml@umh.ac.be>
> > [...] I have some code using objects (visitor pattern), recursive
> > modules, lazyness, and private row types, in an utterly non trivial
> > way, just to do what can be done by standard recursive function
> > definitions using polymorphic variants...
> 
> Sounds like a good case to see & learn the power of polymorphic
> variants in action.  Are the two codes available somewhere (if
> possible with some explanations ?) or are you simply referring to your
> paper "Code reuse through polymorphic variants" ?

Well, I am. Other examples end up being much longer, even using
polymorphic variants :-)

But still, I include at the end of this mail the code to obtain a
fully extensible purely functional polymorphic visitor pattern.
(This is the polymorphic part that is particularly hard, even more
if you want to stay purely functional.)

For comparison, here is the equivalent complete code using polymorphic
variants. Note that there is no explicit visitor pattern: the match
construct provides it, with all the polymorphism needed.

type 'a eadd = [ `Num of int | `Add of 'a * 'a ]
let eval_add eval_rec : 'a eadd -> int = function
  | `Num i -> i
  | `Add (e1, e2) -> eval_rec e1 + eval_rec e2
let rec eval_add' e = eval_add eval_add' e
(* val eval_add' : ('a eadd as 'a) -> int *)
type 'a eaddneg = ['a eadd | `Neg of 'a]
let eval_add_neg eval_rec : 'a eaddneg -> int = function
  | #eadd as e -> eval_add eval_rec e
  | `Neg e -> - eval_rec e
let rec eval_add_neg' e = eval_add_neg eval_add_neg' e
(* val eval_add_neg' : ('a eaddneg as 'a) -> int *)
let n = eval_add_neg' (`Add (`Neg(`Add(`Num 3, `Num 2)), `Num 7))
(* val n : int = 2 *)

This also means that providing a method returning a polymorphic
variant describing the contents of an object is probably a simpler
approach to implementing the visitor pattern, even for objects. Here
is the code needed if you still want to use objects.

class type ['a] expr = object method repr : 'a end
let rec eval_add_expr (e : _ expr) = eval_add eval_add_expr e#repr
(* val eval_add_expr : ('a eadd expr as 'a) -> int *)
let rec eval_add_neg_expr (e : _ expr) = eval_add_neg eval_add_neg_expr e#repr
(* val eval_add_neg_expr : ('a eaddneg expr as 'a) -> int *)

Regards,

Jacques Garrigue

(* A fully extensible polymorphic visitor pattern.
   Code written with Keiko Nakata *)

class type ['a,'exp] visit_add = object
  method visitNum : int -> 'a
  method visitAdd : 'exp -> 'exp -> 'a
end

module type AddTE = sig
  type ('a,'exp) t
  type exp = < accept : 'a. ('a, exp) t -> 'a >
  val num : int -> exp
  val add : exp -> exp -> exp
end

module type AddT = sig
  include AddTE
  val eval : (int, exp) t Lazy.t
end

module AddF(X : AddT with type ('a,'exp) t = private ('a,'exp) #visit_add) =
struct
  type ('a, 'exp) t = ('a, 'exp) X.t
  class type exp = object ('e) method accept : 'a. ('a, 'e) t -> 'a end
  class num x = object (_ : #exp) method accept v = v#visitNum x end
  let num x = new num x
  class add a b = object (_ : #exp) method accept v = v#visitAdd a b end
  let add x = new add x
  class eval = object (eval)
    method private visit (e : exp) = e#accept (Lazy.force X.eval)
    method visitNum (i : int) = i
    method visitAdd r l = eval#visit r + eval#visit l
  end
  let eval = lazy (new eval)
end

module rec Add : AddT with type('a,'exp) t = ('a,'exp) visit_add = AddF(Add)

class type ['a,'exp] visit_add_neg = object
  inherit ['a,'exp] visit_add
  method visitNeg : 'exp -> 'a
end

module type AddNegT = sig
  include AddT
  val neg : exp -> exp
end

module AddNegF(X : AddNegT with
               type ('a,'exp) t = private ('a,'exp) #visit_add_neg) =
struct
  module Add = AddF(X)
  include (Add : AddTE with type ('a,'e) t = ('a,'e) X.t)
  class neg x = object (_ : #Add.exp) method accept v = v#visitNeg x end
  let neg x = new neg x
  class eval = object (eval)
    inherit Add.eval
    method visitNeg e = - eval#visit e
  end
  let eval = lazy (new eval)
end

module rec AddNeg : AddNegT with type ('a,'exp) t = ('a,'exp) visit_add_neg =
  AddNegF(AddNeg)

open AddNeg
let n = (add (neg (add (num 3) (num 2))) (num 7))#accept (Lazy.force eval)

Re: [Caml-list] Polymorphic Variants

[skaller]

On Wed, 2007-01-17 at 11:19 +0900, Jacques GARRIGUE wrote:

> If you mean that, without type annotations, types and errors become
> very hard to read, this is true, but the manual explicitely encourages
> to add type annotations :-)

You are not kidding .. and even type annotations don't always help.
I regularly get 100-200 line errors, even in cases where the compiler
clearly knows which tag is causing the problem.

But I would not give up the polymorphic variants despite this pain,
because the alternative is now unthinkable.

Basically, with ordinary variants if you have some subset
of cases you can handle it easily but verbosely with
morphisms:

	type X = | A | B | C | D
	type Y = | AA | BB

	let XtoY x : Y = match x with
	| A -> AA
	| B -> BB
	| _ -> failwith "blah"

	let YtoX y : X = match y with
	| AA -> A
	| BB -> B


With polymorphic variants these morphisms are created automatically,
and AFAIK the embedding (YtoX) has zero cost. You can also do:

	type X = [`A | `B | `C | `D]
	type Y = [`A | `B]

	let XtoY x: Y = match x with
	| #Y as y -> (y:X:>Y)
	| _ -> failwith "khg"


	let YtoX y: X = (y:Y:>X)

This is mainly "syntactic sugar". The recursive case is where 
polymorphic variants really shine, eg a compiler "expression"
type with various "sub expression" types where there are constraints
satisfied recursively by all nodes. (These things are still far too
hard to define with multiple parameters though .. ;(



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

Re: [Caml-list] Polymorphic Variants

[Andrej Bauer]

skaller wrote:

> You are not kidding .. and even type annotations don't always help.
> I regularly get 100-200 line errors, even in cases where the compiler
> clearly knows which tag is causing the problem.

Pah, that's nothing. An early version of Cduce ocassionally gave me 
error messages that were 1GB (!) in legnth. Now can your Felix do THAT?

Andrej

Re: [Caml-list] Polymorphic Variants

[Tom]

[-- Attachment #1: Type: text/plain, Size: 3329 bytes --]

On 17/01/07, Jacques GARRIGUE <garrigue@math.nagoya-u.ac.jp> wrote:
>
> From: Tom <tom.primozic@gmail.com>
> > So... why actually are polymorphic variants useful? Why can't they
> simply be
> > implemented as normal, concrete (or how would you call them? ...)
> variants?
>
> The original motivation was for the LablTk library, where some types
> (index for instance) have lots of small variations. At that point
> there where several options
> * overloading (but ocaml loathes overloading, you could say that the
>   total absence of overloading is essential to the language)
>

Is there a reason for that? Is it only hard to implement or are there any
conceptual / strategical / theoretical reasons?

> OCaml does not, as far as I know, have any structural typing for
> records..

Hm... Actually, what I had in mind is nominal subtyping... similar to
objects, in fact, objects in C++-like languages, just that they have no
class methods.

Now... close your eyes (but try to continue reading this ;) ) and imagine
you're in a dreamworld. You are programming in a language that has
  * function overloading that allows you to have
       length "abcd" + length [1; 2; 3]
  * Constructor overloading, eliminating the need of
       type parse_expression =
           Pexp_name of string
         | Pexp_constant of constant
         | Pexp_let of (pattern * parse_expression) * parse_expression
         | Pexp_apply of parse_expression * parse_expression list
         | Pexp_try of parse_expression * (pattern * parse_expression) list

       type typed_expression =
           Texp_ident of ident
         | Texp_constant of constant
         | Texp_let of (pattern * typed_expression) * typed_expression
         | Texp_apply of typed_expression * typed_expression list
         | Texp_try of typed_expression * (pattern * typed_expression) list
    as it can be coded as
       type parse_expression =
           Name of string
         | Constant of constant
         | ...

       type typed_expression =
           Ident of ident
         | Constant of constant
         | ...

  * nominal subtyping of records, with overloaded field names:
       type widget = {x : float; y : float; width: float; height: float} (*
top-level type *)
       type button = {widget | text : string }
       type checkbox = {button | checked : bool}
       type image = {widget | url : string}

       type vector = {x : float; y : float}
       type document {url : url}

    so subtypes could be applied to a function
       fun move : widget -> (float * float) -> unit

       let chk = {x = 0.0; y = 0.0; width = 10.0; height = 12.0; text =
"Check me!"; checked = false}
       move chk (3.0, 3.0)
    and types could be "discovered" at runtime:
       let draw widget =
         typematch widget with
             w : widget -> draw_box (w.x, w.y, w.height, w.width)
           | b : button -> draw_box (b.x, b.y, b.height, b.width); draw_text
b.text
           | i : image -> draw_image i.url (i.x, i.y)
           | ...

Do you think you would be "satisfied" even without polymorphic variants?

I am not saying this just for fun... I want to create a language with
overloading, but I kinda don't really like polymorphic variants... thou if
they turn out to be really useful, I would probably start to like them.

Any comments?

- Tom

[-- Attachment #2: Type: text/html, Size: 5258 bytes --]

Re: [Caml-list] Polymorphic Variants

[Jon Harrop]

On Wednesday 17 January 2007 21:13, Tom wrote:
> Any comments?

Yes: I prefer things the way they are.

You can add overloading to ML but you must then add lots of type annotations 
to your code. For example, vector length:

  let length (x, y) = sqrt(x*.x +. y*.y)

becomes:

  let length (x : float, y : float) = sqrt(x*x + y*y)

So you've saved the "." three times at the cost of ": float" twice because the 
overloaded * and + don't provide enough type information. You can complicate 
the type inferer to counteract this but then other type errors will become 
increasingly obscure and the programmer will be forced to learn the quirks 
that you've added in order to debug their code.

Constructor overloading can be done in OCaml using polymorphic variants. They 
are slower. Code written in this style quickly becomes unmaintainable because 
the type errors (from inference) are so complicated that you are forced to 
annotate types.

Finally, I don't want my types discovered at run-time because it makes my code 
slower and uses more memory. I'd rather have to box manually, so fast code is 
concise code.

From my point of view, your suggestions are mostly steps backwards (towards 
Lisp, C++ etc.).

I think the best way to improve OCaml is to write an IDE that sidesteps these 
problems, e.g. by typesetting the code "+." as "+".

-- 
Dr Jon D Harrop, Flying Frog Consultancy Ltd.
Objective CAML for Scientists
http://www.ffconsultancy.com/products/ocaml_for_scientists

Re: [Caml-list] Polymorphic Variants

[Tom]

[-- Attachment #1: Type: text/plain, Size: 1557 bytes --]

>
>
> Yes: I prefer things the way they are.


I don't mean an revolution. Rather a symbiosys.

You can add overloading to ML but you must then add lots of type annotations
> to your code. For example, vector length:
>
>   let length (x, y) = sqrt(x*.x +. y*.y)
>
> becomes:
>
>   let length (x : float, y : float) = sqrt(x*x + y*y)
>
> So you've saved the "." three times at the cost of ": float" twice because
> the
> overloaded * and + don't provide enough type information. You can
> complicate
> the type inferer to counteract this but then other type errors will become
> increasingly obscure and the programmer will be forced to learn the quirks
> that you've added in order to debug their code.


3 solutions:
  * sqrt has type of float -> float and the compiler infers float arguments
  * you write +. and *. (at least once) (those operators could be still
available, don't you think so?)
  * let the compiler overload your function ( length : (int * int) -> float;
length : (float * float) -> float) and then drop the "int" one as you never
ever used it in your code.


> Finally, I don't want my types discovered at run-time because it makes my
> code
> slower and uses more memory. I'd rather have to box manually, so fast code
> is
> concise code.


More memory is used by polymorphic variants too. And the records could be
optimised so that type information is only added when it is needed by the
programm.

>From my point of view, your suggestions are mostly steps backwards (towards
> Lisp, C++ etc.).


Thank you for your comment :)

- Tom

[-- Attachment #2: Type: text/html, Size: 2336 bytes --]

Fwd: [Caml-list] Polymorphic Variants

[Tom]

[-- Attachment #1: Type: text/plain, Size: 4655 bytes --]

---------- Forwarded message ----------
From: Tom <tom.primozic@gmail.com>
Date: 18-Jan-2007 13:07
Subject: Re: [Caml-list] Polymorphic Variants
To: Jon Harrop <jon@ffconsultancy.com>



On 18/01/07, Jon Harrop <jon@ffconsultancy.com> wrote:

> On Wednesday 17 January 2007 23:07, you wrote:
> > 3 solutions:
> >   * sqrt has type of float -> float and the compiler infers float
> arguments
>
> Type inference starts at the leaf subexpressions. In the absence of other
> type
> information, it gets to x*x and infers x to be the default type parameter
> of
> + and then fails when it gets to sqrt of an int.


No... i rather thought it that way:
     x is anything
     x * x is either int or float, so x is either int or float
     x * x + x * x is either int or float, so the two (x * x) are either
both int or both float
     sqrt accepts a float argument, so x * x + x * x must be float, so (x *
x) must be float, so x must be float.



> >   * you write +. and *. (at least once) (those operators could be still
> > available, don't you think so?)
>
> Yes. Then you have complicated the language without improving upon OCaml.


Hm... well, I must say that I agree. Actually, I am against this option (for
purposes other that compatibility with original OCaml)



> You could even add a float literal:
>
> x +. 0.


and have it optimized away


>
> > And the records could be
> > optimised so that type information is only added when it is needed by
> the
> > programm.
>
> Then you acquire the poor optimisability of Lisp, where you are forced to
> plough through reams of optimisation-related compiler warnings in order to
> find exactly where you must annotate the code to recover the lost
> performance.


Well... I guess it's quite simple. If it's only one record, than optimise
it. If it has "subrecords" (=subtypes), than don't.

You see, I am not against OCaml. No! I love it. And I am not trying to
change it. You seem to be a priori against my ideas, just because they are
not what is generally accepted. All I want to do is write my own language,
both for the sake of writing one (they say it's good practice) and for the
sake of correcting things that I have found bother me when I program OCaml.
As pointed out a number of times, you should design a language for yourself,
not for others, not for the "general public" [1]. So what I want is
something that will enable me to program in a fast, yet efficient manner,
and to be able to express many things as naturally as possible. Therefore,
most of the features I suggested are not "evil" or "mean", they are just my
solutions to what I think are the most common problems - actually, one
biggest problem: too much typing. No, actually, the nominal subtyping of
records is because it's faster than structural subtyping of objects, as
implemented by OCaml. If anyone has any idea, how to make structural
subtyping faster, I would love to incorporate it.



> >   * let the compiler overload your function ( length : (int * int) ->
> > float; length : (float * float) -> float) and then drop the "int" one as
>
> > you never ever used it in your code.
>
> What happens at code boundaries? e.g. to compile a DLL, the compiler must
> generate all possible permutation of type variables for every function.
> Then
> you end up with a compiler that's 2,000x slower than OCaml's, like the
> Stalin
> scheme compiler.


In addition to what I have written in the previous remark, I think you are
overly concerned with performance only. It's great you think about many
things, but these things have quite simple answers. Either, one could write
an incremental compiler (similar to the way OCaml provides separate
compilation, but somehow more refined is what I have in mind), or write
interfaces - again what OCaml does (to optimise say, the min function (let
min (x: int) y = if x > y then y else x) so that it is faster) - it's just
that what you would actually need to do is DELETE interfaces, because the
compiler would infer the whole interface for you, and you would just delete
the entries you don't want to have in it.

All in all, I believe that optimizations (compile-time evaluation (and don't
say I forgot that some functions have side effects)), incremental
compilation and a smart and powerful IDE, along with OCaml's already
existent debugger and profiler should keep one from being stopped by
implementation issues. Idea, ideas, ideas are important, ideas are what
matters.

[1] http://www.paulgraham.com/langdes.html (2. Design for Yourself and Your
Friends. )


By the way, do you think I can send this message to others too? (I think it
significantly clarifies my position)

- Tom

[-- Attachment #2: Type: text/html, Size: 6774 bytes --]

Re: Fwd: [Caml-list] Polymorphic Variants

[Jon Harrop]

On Thursday 18 January 2007 16:23, Tom wrote:
> No... i rather thought it that way:
>      x is anything
>      x * x is either int or float, so x is either int or float
>      x * x + x * x is either int or float, so the two (x * x) are either
> both int or both float
>      sqrt accepts a float argument, so x * x + x * x must be float, so (x *
> x) must be float, so x must be float.

Much better. Except I want + to work on int, float, float32, 'a^n (static 
vectors), 'a^n^m (static matrices), 'a array, 'a list, 'a set. Not only that, 
I want + and * to work on two values of different types: date+time, 
float*vector and so on.

Hell, I want to overload 0 to mean 0, 0., 0. + 0.i, zero vector and the zero 
matrix. Of course, the zero matrix has arbitrary dimensionalities that could 
be static, so my type now contains variables for those.

Now, where your type inferencer had a simple type expression or atom (int or 
float), it can have expressions of mutually-recursive sets of type 
expressions.

You see how things will get more complicated to define correctly, slower to 
compile and much harder to comprehend when things go wrong? You've opened a 
whole can of worms. Some of those worms look tasty but you either eat them 
all or you put them all back.

> > You could even add a float literal:
> >
> > x +. 0.
>
> and have it optimized away

No, because x+0=x is not true for all floats:

# -0. +. 0.;;
- : float = 0.

> You see, I am not against OCaml. No! I love it. And I am not trying to
> change it. You seem to be a priori against my ideas, just because they are
> not what is generally accepted.

Not at all. They are very good ideas on the surface. The problem is what costs 
lay hidden beneath the surface in an implementation of such a language.

> All I want to do is write my own language, 
> both for the sake of writing one (they say it's good practice) and for the
> sake of correcting things that I have found bother me when I program OCaml.
> As pointed out a number of times, you should design a language for
> yourself, not for others, not for the "general public" [1].

Ok.

> So what I want 
> is something that will enable me to program in a fast, yet efficient
> manner, and to be able to express many things as naturally as possible.
> Therefore, most of the features I suggested are not "evil" or "mean", they
> are just my solutions to what I think are the most common problems -
> actually, one biggest problem: too much typing.

Then I think you need to choose bigger examples in order to weigh the 
reduction in code size that you've seen with the increase in code size due to 
type annotations.

> No, actually, the nominal 
> subtyping of records is because it's faster than structural subtyping of
> objects, as implemented by OCaml.

That's a good idea. I'd like to have vec2 and vec3 records that reused x and y 
field names.

> If anyone has any idea, how to make 
> structural subtyping faster, I would love to incorporate it.

Right. I think structural subtyping is a good complement to the rest of 
OCaml's type system.

> > What happens at code boundaries? e.g. to compile a DLL, the compiler must
> > generate all possible permutation of type variables for every function.
> > Then
> > you end up with a compiler that's 2,000x slower than OCaml's, like the
> > Stalin
> > scheme compiler.
>
> In addition to what I have written in the previous remark, I think you are
> overly concerned with performance only.

I am, yes. OCaml's designers were too, I think.

> It's great you think about many 
> things, but these things have quite simple answers. Either, one could write
> an incremental compiler (similar to the way OCaml provides separate
> compilation, but somehow more refined is what I have in mind), or write
> interfaces - again what OCaml does (to optimise say, the min function (let
> min (x: int) y = if x > y then y else x) so that it is faster) - it's just
> that what you would actually need to do is DELETE interfaces, because the
> compiler would infer the whole interface for you, and you would just delete
> the entries you don't want to have in it.

Good idea. Not having to repeat types in .mli files would be an improvement, 
IMHO.

> All in all, I believe that optimizations (compile-time evaluation (and
> don't say I forgot that some functions have side effects)), incremental
> compilation and a smart and powerful IDE, along with OCaml's already
> existent debugger and profiler should keep one from being stopped by
> implementation issues. Idea, ideas, ideas are important, ideas are what
> matters.

Absolutely. I would welcome a decent OCaml IDE. I've even considered writing 
one a few times, but you'd need a good GPU to run mine. ;-)

-- 
Dr Jon D Harrop, Flying Frog Consultancy Ltd.
Objective CAML for Scientists
http://www.ffconsultancy.com/products/ocaml_for_scientists

Re: Fwd: [Caml-list] Polymorphic Variants

[Dirk Thierbach]

On Thu, Jan 18, 2007 at 09:14:09PM +0000, Jon Harrop wrote:
> On Thursday 18 January 2007 16:23, Tom wrote:

>> No... i rather thought it that way:
>>      x is anything
>>      x * x is either int or float, so x is either int or float
>>      x * x + x * x is either int or float, so the two (x * x) are either
>> both int or both float
>>      sqrt accepts a float argument, so x * x + x * x must be float, so (x *
>> x) must be float, so x must be float.

BTW, that's what Haskell's type classes do:

Prelude> :t \x -> x
\x -> x :: forall t. t -> t

Prelude> :t \x -> x * x
\x -> x * x :: forall a. (Num a) => a -> a
Prelude> :t \x -> (x * x) + (x * x)
\x -> (x * x) + (x * x) :: forall a. (Num a) => a -> a

Prelude> :t \x -> sqrt x
\x -> sqrt x :: forall a. (Floating a) => a -> a

In the first case, x can have any type. In the next two, it must be
a number (int, float, etc.). In the last case, it must be a specific kind
of number, namely "float-like", which includes (single precision) Float, 
Double, and Complex.

> Much better. Except I want + to work on int, float, float32, 'a^n
> (static vectors), 'a^n^m (static matrices), 'a array, 'a list, 'a
> set. Not only that, I want + and * to work on two values of
> different types: date+time, float*vector and so on.

Sure. Just write the apropriate instances for the type class, if
it isn't defined already. Encoding dimensionalities into types
can require a bit of magic :-)

> Hell, I want to overload 0 to mean 0, 0., 0. + 0.i, zero vector and
> the zero matrix. 

No problem either: Number literals like "0" are translated into the 
expression "fromInteger 0", so by overloading fromInteger in the
type class, you can generate the apropriate constant.

> Of course, the zero matrix has arbitrary dimensionalities that could
> be static, so my type now contains variables for those.

Again, no problem.

Of course, you pay for that flexibility by having to pass around 
dictionaries at runtime (unless you specialize early, or the compiler
is really clever about inlining and specializing).

> You see how things will get more complicated to define correctly, slower to 
> compile and much harder to comprehend when things go wrong? 

Certainly. One has to be very careful what to allow and what to disallow.
But at least those very basic examples work fine.

- Dirk

Re: Fwd: [Caml-list] Polymorphic Variants

[Tom]

[-- Attachment #1: Type: text/plain, Size: 2098 bytes --]

On 19/01/07, Dirk Thierbach <dthierbach@gmx.de> wrote:
>
> On Thu, Jan 18, 2007 at 09:14:09PM +0000, Jon Harrop wrote:
> > On Thursday 18 January 2007 16:23, Tom wrote:
>
> >> No... i rather thought it that way:
> >>      x is anything
> >>      x * x is either int or float, so x is either int or float
> >>      x * x + x * x is either int or float, so the two (x * x) are
> either
> >> both int or both float
> >>      sqrt accepts a float argument, so x * x + x * x must be float, so
> (x *
> >> x) must be float, so x must be float.
>
> BTW, that's what Haskell's type classes do:



Well, in some sense, generic value overloading is somewhat like Haskell's
type classes, with an advantage that type classes are infered automatically
by the compiler (or, actually, are not named/declared - the compiler simply
lists all types belonging to the current typeclass

Prelude> :t \x -> x
> \x -> x :: forall t. t -> t
>
> Prelude> :t \x -> x * x
> \x -> x * x :: forall a. (Num a) => a -> a


     forall a . (int, float, complex, fraction, bignum, int32, vector2,
vector3, string) => a -> a

or, what I would prefer:

     [int -> int | float -> float | complex -> complex | fraction ->
fraction | bignum -> bignum | int32 -> int32 | vector2 -> vector2 | vector3
-> vector3 | string -> string]

(Yes, it seems a lot of writing... but remember that it is not you who
writes that, it's the compiler. While for such short types, a -> a,
Haskell's notation is better, it could become hard to understand with more
complex types:
     forall a . (float, complex, fraction) => forall b . (int, string) => a
-> a -> b -> b -> (a, b)
Now, go figure all the possibilities... It's much simpler when the compiler
lists all the combinations for you.

> Hell, I want to overload 0 to mean 0, 0., 0. + 0.i, zero vector and
> > the zero matrix.
>
> No problem either: Number literals like "0" are translated into the
> expression "fromInteger 0", so by overloading fromInteger in the
> type class, you can generate the apropriate constant.


Can Haskell overload values? And functions by their return type?

- Tom

[-- Attachment #2: Type: text/html, Size: 3124 bytes --]

Re: Fwd: [Caml-list] Polymorphic Variants

[Dirk Thierbach]

[Please don't reply directly to me AND to the list, just to the list
is enough. Thanks.]

On Fri, Jan 19, 2007 at 11:35:36AM +0100, Tom wrote:
> On 19/01/07, Dirk Thierbach <dthierbach@gmx.de> wrote:

> Well, in some sense, generic value overloading is somewhat like Haskell's
> type classes, 

Yes. That's exactly what type classes are for -- overloading of functions
(including infix operators).

> Prelude> :t \x -> x
> >\x -> x :: forall t. t -> t
> >
> >Prelude> :t \x -> x * x
> >\x -> x * x :: forall a. (Num a) => a -> a

>     forall a . (int, float, complex, fraction, bignum, int32, vector2,
> vector3, string) => a -> a

That's both longer and not extensible -- what if you're going to link
a module the offers matrices? Don't you also want to use the function
in that context?

> or, what I would prefer:
> 
>     [int -> int | float -> float | complex -> complex | fraction ->
> fraction | bignum -> bignum | int32 -> int32 | vector2 -> vector2 | vector3
> -> vector3 | string -> string]

That's even worse :-)

> (Yes, it seems a lot of writing... but remember that it is not you who
> writes that, it's the compiler. While for such short types, a -> a,
> Haskell's notation is better, it could become hard to understand with more
> complex types:

>     forall a . (float, complex, fraction) => forall b . (int, string) => a
> -> a -> b -> b -> (a, b)

> Now, go figure all the possibilities... It's much simpler when the compiler
> lists all the combinations for you.

And that's exactly what the Haskell compiler does (see below). BTW,
the important thing is the type variable after the predicate, just
ignore the forall's for the moment. So the above type is nonsense, a
possible example type could look like:

(Num a, Floating b) => a -> a -> b -> b -> (a, b)

And it's quite easy to read: The function itself has type 

a -> a -> b -> b -> (a, b)

where all the a's represent the same type, and all the b's represent
the same type, as usual in type inference. Moreover, every concrete
type for "a" must be an instance of Num (i.e., float, complex,
fraction, whatever, you don't care -- the important point is that it
is "a number"), and "b" must be a instance of Floating (same idea).

> >Hell, I want to overload 0 to mean 0, 0., 0. + 0.i, zero vector and
> >> the zero matrix.
> >
> >No problem either: Number literals like "0" are translated into the
> >expression "fromInteger 0", so by overloading fromInteger in the
> >type class, you can generate the apropriate constant.

> Can Haskell overload values? And functions by their return type?

It can overload integer and fixed point literals (in the way described
above). It cannot overload any other "values" (whatever that should
be :-). And yes, it can overload functions by their return type:

Num a => Integer -> a

is a legal type (for example, it's the type of the function "fromInteger"). 
It really doesn't matter if the type variable "a" appears as argument
or as the result (or, more generally, in a covariant or contravariant
position).

If you want more details, I'd recommend to have a look at the Haskell 
docs or tutorials.

- Dirk

Re: Fwd: [Caml-list] Polymorphic Variants

[Tom]

[-- Attachment #1: Type: text/plain, Size: 2497 bytes --]

On 19/01/07, Dirk Thierbach <dthierbach@gmx.de> wrote:
>
> [Please don't reply directly to me AND to the list, just to the list
> is enough. Thanks.]


Sorry... didn't mean to... I mean, I didn't know there's a problem. I don't
get mail that's sent to me AND the caml-list twice...

On Fri, Jan 19, 2007 at 11:35:36AM +0100, Tom wrote:
> > On 19/01/07, Dirk Thierbach <dthierbach@gmx.de> wrote:
>
> > Well, in some sense, generic value overloading is somewhat like
> Haskell's
> > type classes,
>
> Yes. That's exactly what type classes are for -- overloading of functions
> (including infix operators).


No, no, you misunderstood me. Type-classes are run-time dispatched. What I
want is static/compile-time overloading. I meant they are similar for the
type inference system. My type system should use roughly the same algorithm
for inference that Haskell uses, but it should infer the typeclasses (the
possible types a type variable can be instantiated) automatically.

Actually, I don't even want such types be extensible - one function will
always have either ONE input type (int -> int), or ANY input types ('a ->
'a), but two such functions might have the same NAME. The compiler's task
isn't to supply all possible implementations of some mathematical function -
that's the programmers task:

if I define
  let negate a = - a
it will not have all possible types (int, float, complex, ...) but only one
of them. For another type, I have to define it again:
  let negate a = - a
I can also specify types:
  let negate a : complex = - a
(and of course ask the compiler to do it for me:
  overload let negate a = - a
but that's only a shortcut - internally, it would be expanded into n
functions, each ranging over one of n types. )

My overloading would be more C++ / C# / Java-like - but the inference
technique should be similar to Haskell's.

And that's exactly what the Haskell compiler does (see below).




BTW,
> the important thing is the type variable after the predicate, just
> ignore the forall's for the moment. So the above type is nonsense, a
> possible example type could look like:


Sorry, I don't know Haskell that well. But you know what I meant :)


> > Can Haskell overload values? And functions by their return type?
>
> It can overload integer and fixed point literals (in the way described
> above). It cannot overload any other "values" (whatever that should
> be :-).


By overloading values, I mean:

let null = 0
let null = false

if null then 1 else null

- Tom

[-- Attachment #2: Type: text/html, Size: 3891 bytes --]

Re: [Caml-list] Polymorphic Variants

[Christophe TROESTLER]

On Wed, 17 Jan 2007, Jon Harrop <jon@ffconsultancy.com> wrote:
> 
> I think the best way to improve OCaml is to write an IDE that sidesteps these 
> problems, e.g. by typesetting the code "+." as "+".

Tuareg can do it.  Just put

  (setq tuareg-font-lock-symbols t)

in the appropriate section of your ~/.emacs

ChriS

Re: [Caml-list] Polymorphic Variants

[Jacques Garrigue]

From: Tom <tom.primozic@gmail.com>
> On 17/01/07, Jacques GARRIGUE <garrigue@math.nagoya-u.ac.jp> wrote:
> > From: Tom <tom.primozic@gmail.com>
> > > So... why actually are polymorphic variants useful? Why can't they
> > simply be
> > > implemented as normal, concrete (or how would you call them? ...)
> > variants?
> >
> > The original motivation was for the LablTk library, where some types
> > (index for instance) have lots of small variations. At that point
> > there where several options
> > * overloading (but ocaml loathes overloading, you could say that the
> >   total absence of overloading is essential to the language)
> 
> Is there a reason for that? Is it only hard to implement or are there any
> conceptual / strategical / theoretical reasons?

There are two kinds of theoretical reasons.

The most theoretical one is about semantics: with generic overloading,
all your semantics must take types into account. This is a problem as
most theoretical studies of lambda-calculus are based on so-called
erasure semantics, where types are discarded at execution. So this
means you must design your own, more complex semantics. Not that this
reason may not apply to constructor or record overloading, if you do
not allow the semantics to change according to the type.

The other one is about type inference. Basically, overloading has a
huge impact on overloading. The direct way to handle it, using types
alone, is deeply disruptive, as it means that some programs will be
refused for lack of type information. It is very hard to define a
clear criterion on which programs should be refused, notwithstanding
internal details of the compiler. This also applies to record and
constructor overaloading. There are other approach the problem, with
constrained type variables (either Haskell's type classes or G'Caml's
generic type variables,) but of course they add complexity to the type
system. And it is not clear that they solve the problem for
constructor and record overloading: in Haskell, records fields are not
overloaded, and constructor overloading has to be done by hand for
each type, through an explicit encoding into type classes.

Both reasons have practical impact. For the first one, using erasure
semantics means that the programmer also can discard types when
understanding the runtime behaviour of a program. For the second one,
you can write code that is maximally polymorphic, without too much
fear about the impact of performance (equality is overloaded, so
it still matters...) or strange ambiguity-related error messages.

So for the time being ocaml keeps to no overloading at all.

> > OCaml does not, as far as I know, have any structural typing for
> > records..

Not for records, but for objects. From a type-theoretic point of view
they are just equivalent.

> Hm... Actually, what I had in mind is nominal subtyping... similar to
> objects, in fact, objects in C++-like languages, just that they have no
> class methods.

Reading the description below, this all looks nice, independently of
the semantics limitation described above. However, you can kiss
farewell to type inference. With such an extensive overloading, you
would need type annotations all over the place.
By the way, this all looks likes the "used this feature in C++"
syndrome. Sure C++ is incredibly powerful. But it is built on rather
shaky theoretical fundations. So you can't expect to bring everything
from C++ to a new language. Why not think about new ways to solve
problems :-)
(To be completely honest, this also looks a bit like ML2000, and the
Moby language, which has a sound theoretical fundation, but never
really took off. You might want to go see for yourself.)

Jacques Garrigue
 
> Now... close your eyes (but try to continue reading this ;) ) and imagine
> you're in a dreamworld. You are programming in a language that has
>   * function overloading that allows you to have
>        length "abcd" + length [1; 2; 3]
>   * Constructor overloading, eliminating the need of
>        type parse_expression =
>            Pexp_name of string
>          | Pexp_constant of constant
>          | Pexp_let of (pattern * parse_expression) * parse_expression
>          | Pexp_apply of parse_expression * parse_expression list
>          | Pexp_try of parse_expression * (pattern * parse_expression) list
> 
>        type typed_expression =
>            Texp_ident of ident
>          | Texp_constant of constant
>          | Texp_let of (pattern * typed_expression) * typed_expression
>          | Texp_apply of typed_expression * typed_expression list
>          | Texp_try of typed_expression * (pattern * typed_expression) list
>     as it can be coded as
>        type parse_expression =
>            Name of string
>          | Constant of constant
>          | ...
> 
>        type typed_expression =
>            Ident of ident
>          | Constant of constant
>          | ...
> 
>   * nominal subtyping of records, with overloaded field names:
>        type widget = {x : float; y : float; width: float; height: float} (*
> top-level type *)
>        type button = {widget | text : string }
>        type checkbox = {button | checked : bool}
>        type image = {widget | url : string}
> 
>        type vector = {x : float; y : float}
>        type document {url : url}
> 
>     so subtypes could be applied to a function
>        fun move : widget -> (float * float) -> unit
> 
>        let chk = {x = 0.0; y = 0.0; width = 10.0; height = 12.0; text =
> "Check me!"; checked = false}
>        move chk (3.0, 3.0)
>     and types could be "discovered" at runtime:
>        let draw widget =
>          typematch widget with
>              w : widget -> draw_box (w.x, w.y, w.height, w.width)
>            | b : button -> draw_box (b.x, b.y, b.height, b.width); draw_text
> b.text
>            | i : image -> draw_image i.url (i.x, i.y)
>            | ...
> 
> Do you think you would be "satisfied" even without polymorphic variants?
> 
> I am not saying this just for fun... I want to create a language with
> overloading, but I kinda don't really like polymorphic variants... thou if
> they turn out to be really useful, I would probably start to like them.
> 
> Any comments?
> 
> - Tom

Re: [Caml-list] Polymorphic Variants

[Jon Harrop]

On Thursday 18 January 2007 01:28, Jacques Garrigue wrote:
> ...ML2000...

What did happen to ML2000? Is it on a desert island with JPEG2000 and Fortran 
2000?

-- 
Dr Jon D Harrop, Flying Frog Consultancy Ltd.
Objective CAML for Scientists
http://www.ffconsultancy.com/products/ocaml_for_scientists

Re: [Caml-list] Polymorphic Variants

[skaller]

On Thu, 2007-01-18 at 10:28 +0900, Jacques Garrigue wrote:
> From: Tom <tom.primozic@gmail.com>

> > > * overloading (but ocaml loathes overloading, you could say that the
> > >   total absence of overloading is essential to the language)
> > 
> > Is there a reason for that? Is it only hard to implement or are there any
> > conceptual / strategical / theoretical reasons?
> 
> There are two kinds of theoretical reasons.
> 
> The most theoretical one is about semantics: with generic overloading,
> all your semantics must take types into account. This is a problem as
> most theoretical studies of lambda-calculus are based on so-called
> erasure semantics, where types are discarded at execution. 

Can you explain this more? The kind of overloading I'm used
to is a matter of lookup not semantics, i.e. its just syntactic
sugar to save the human reader's memory.

> Reading the description below, this all looks nice, independently of
> the semantics limitation described above. However, you can kiss
> farewell to type inference. With such an extensive overloading, you
> would need type annotations all over the place.

Felix makes this tradeoff. Types are deduced bottom up (s-attributes),
so variables and function return types are calculated, but function
parameters must be explicitly typed.

Even in Ocaml it is necessary to write some annotations
in two cases:

(a) hard to understand error messages from type inference

(b) polymorphic variants

On point (a) I admit I often *remove* the annotations
after writing them (which I can't do in Felix). The need
for (b) is limited and quite acceptable IMHO, it just takes
a bit more experience than I have to pick when you need
annotations or explicit coercions.

On the other hand some code would just be impossible
without overloading. For example C has

	char, short, int, long, long long
	unsigned versions
	float, double, long double

which is 13 distinct 'number' types, and I would hate
to have to write:

	1 int_add 2
	1L long_add 2L

Similarly I have had a 'pretty printer' program which prints
terms of an AST (the Felix grammar actually) and the fact I
could overload

	fun str : t -> string

meant I could usually forget what type it was I was converting
to a string. (There are something like 50 AST node types 
involved I think).

So in some cases with inference and without overloading,
*you need the annotations anyhow*, they just go into the
function names in an unprincipled manner, instead of going
into the function parameter types in a principled -- 
and indeed syntactically enforced -- manner.

Overall Felix library function declarations are considerably
more verbose than Ocaml .. but the implementation is about
the same complexity.

BTW: of course in Ocaml you can add annotations for documentation
purposes or to enforce a constraint.

> By the way, this all looks likes the "used this feature in C++"
> syndrome. 

Actually for Felix this is a legitimate reason :)

> Sure C++ is incredibly powerful. But it is built on rather
> shaky theoretical fundations.

What? C++ has theoretical foundations? 

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

Re: [Caml-list] Polymorphic Variants

[Jacques Garrigue]

From: skaller <skaller@users.sourceforge.net>

> > The most theoretical one is about semantics: with generic overloading,
> > all your semantics must take types into account. This is a problem as
> > most theoretical studies of lambda-calculus are based on so-called
> > erasure semantics, where types are discarded at execution. 
> 
> Can you explain this more? The kind of overloading I'm used
> to is a matter of lookup not semantics, i.e. its just syntactic
> sugar to save the human reader's memory.

Because you're doing some partial evaluation :-)
Namely you can view an overloaded function as a function taking extra
hidden parameters: the types of its arguments. If these types are
monomorphic, then you can immediately partially evaluate your function
to choose the right implementation. But if they are polymorphic, you
need to pass extra information around. This is what is done in Haskell
for instance, passing dictionnaries for type classes.
So an alternative view is that overloading is a type dependent
translation from the source code to an explicit version. You can only
drop the types after this translation. So this means that you cannot
understand the source code locally: you need to be aware of the type
information around it.

> > Reading the description below, this all looks nice, independently of
> > the semantics limitation described above. However, you can kiss
> > farewell to type inference. With such an extensive overloading, you
> > would need type annotations all over the place.
> 
> Felix makes this tradeoff. Types are deduced bottom up (s-attributes),
> so variables and function return types are calculated, but function
> parameters must be explicitly typed.

This works if you don't add either subtyping or return-type
overloading to the mix. Then you must also know the type of variables
and the return type of functions. 

> Even in Ocaml it is necessary to write some annotations
> in two cases:
> 
> (a) hard to understand error messages from type inference
> 
> (b) polymorphic variants

This is not exactly the same thing, as these annotations have no
impact on the semantics. Of course, one could say: if we have the
annotation, why not use it for the semantics? But this is another
story, with different implications.

> On the other hand some code would just be impossible
> without overloading. For example C has
> 
> 	char, short, int, long, long long
> 	unsigned versions
> 	float, double, long double
> 
> which is 13 distinct 'number' types, and I would hate
> to have to write:
> 
> 	1 int_add 2
> 	1L long_add 2L

Actually this is not only overloading that is used here, but also
automatic conversions. When writing numeric computations in ocaml, I
find it just as painful to have to add float_of_int, as to add the dot
after all operators. (In number of characters, float_of_int might be
the biggest...)
For overloading alone, the module system could help.
If we had the operators defined with different types in each of the
numeric type modules, then one could just choose the numeric type used
with "open Mynumtype". This is one of the reasons I pushed for having
a local "let open" construct... which can be simulated by "let
module", at a slight cost.

> So in some cases with inference and without overloading,
> *you need the annotations anyhow*, they just go into the
> function names in an unprincipled manner, instead of going
> into the function parameter types in a principled -- 
> and indeed syntactically enforced -- manner.

I believe this is the strongest argument for overloading: that it
allows using types in a principled way. Of course, whether this is
really principled depends on the code you write...

Jacques Garrigue

Re: [Caml-list] Polymorphic Variants

[skaller]

On Thu, 2007-01-18 at 15:20 +0900, Jacques Garrigue wrote:
> From: skaller <skaller@users.sourceforge.net>

> > On the other hand some code would just be impossible
> > without overloading. For example C has
> > 
> > 	char, short, int, long, long long
> > 	unsigned versions
> > 	float, double, long double
> > 
> > which is 13 distinct 'number' types, and I would hate
> > to have to write:
> > 
> > 	1 int_add 2
> > 	1L long_add 2L
> 
> Actually this is not only overloading that is used here, but also
> automatic conversions.

In C/C++ yes, both overloading and automatic conversions.
In Felix there are no automatic conversions.

However Felix still allows you to write

	1 + 1L

if you open the module 'MixedInt'. That module provides
a constrained polymorphic function:

  fun add[t1:fast_ints, t2:fast_ints]: 
    t1 * t2 -> arithmax(t1,t2)
    ="$1+$2"
  ;

where 'fast_ints' is a typeset, which is a finite set
of concrete types, and 

	t: typeset

in this context means

	t where t isin typeset

(which is also legal Felix).

This is, in effect, the complete set of all the 100 overloads 
on the 10 C integer type pairs, represented as polymorphism 
with a constraint checked at the point of call. 

Note the implementation here is "$1+$2" which leverages
C++ overloading.

Typesets and constrained polymorphism are just a convenient
sugar for writing huge numbers of overloads out.

It is interesting that to model the C/C++ type system
here I had to do some quite advanced type system hackery,
but the result is mixed mode arithmetic without any
automatic conversions.

It is also possible to defer choice of types to the instantiation
phase, which can now be done in a well principled manner using
Felix typeclasses. In particular you can now, finally, after
6 years work, do a 'fold' on an STL container using typeclasses
without needing any 'dependent name lookup'.

this is not first class polyadic programming, since (unlike Haskell?)
only types can be typeclass parameters, not functors 
(type constructors, eg STL vector, list, set etc can't be arguments).

However the result is easier to use than Ocaml I think: 
typeclasses are weaker than Ocaml functors but they're much
easier to use, since they work with 'ordinary' code. 

In Ocaml to write 'generic' code you have to put your code 
inside a functor definition. Perhaps that is easy if you have,
for example, one container type, but typical programs will
use several container types, which would require several
levels of nested functors in Ocaml.

I think this would mean that the Ocaml code would be fragile
in the sense that you'd have to do a lot of housekeeping
if the implementation changed to use a slighly different
set of containers -- you'd have to rewrite all the
nested functor wrappers.

I wonder if there is a better way? I really don't like
typeclasses that much: they only allow a single instantiation.
For example

	1 < 2

is an instance of a total ordering typeclass for integers,
but integers can also be sorted in the other direction.
You can't have both orderings, instead you need a dummy
type

	type revint  = RevInt of int 

which supports the reverse ordering. Whereas with Ocaml/ML
functors the comparison function is a specific argument.
I think this is correct.

Hmm .. am I right in thinking Ocaml's local modules also allow
local functor instantiations? This must help quite a bit?

Having to explicitly instantiate is quite a pain though,
compared to C++ templates, typeclasses in either Haskell
or Felix, or plain old Ocaml polymorphic functions:
people keep asking for a polymorphic version of the 
Ocaml Set .. and I'm sure I use Hashtbl polymorphic version
to avoid having to instantiate Map all over the place ***

*** This is not so trivial due to lack of inter module
recursion across ml file boundaries

I wonder if Ocaml couldn't support automatic functor instantiation
by providing an "canonical" instance. For example:

module IntSet = Set.Make (Int)
module FloatSet = Set.Make (Float)

let s1 = IntSet.add s1 1            (* uses manual instantiation *)
let s2 = Set.Make(Int).add s 1      (* uses canonical instantiation *)

The canonical instantiation is 'generated' by the compiler.
It would have to be shared across ml files.

This would be similar to having nominally typed records BUT
also having a canonical structurally typed instance,
namely tuples.


>  When writing numeric computations in ocaml, I
> find it just as painful to have to add float_of_int, as to add the dot
> after all operators. (In number of characters, float_of_int might be
> the biggest...)

Nah, Felix uses BigInt internally for integers in case constants
fit in C integer types but not Ocaml ones .. BigInt.int_of_bigint
is bigger .. :)

> For overloading alone, the module system could help.
> If we had the operators defined with different types in each of the
> numeric type modules, then one could just choose the numeric type used
> with "open Mynumtype".

Yes. Interestingly in Felix you can open both modules
and typeclasses, AND you can partially specialise type
parameters if they're polymorphic, AND these things
can be overloaded .. all at once!

This can be a bit confusing .. especially since the typeclass
feature is new and undoubtedly contains bugs.

>  This is one of the reasons I pushed for having
> a local "let open" construct... which can be simulated by "let
> module", at a slight cost.

Right. You want to localise the impact. Using 'open'
is only "poor man's genericity" but a localised version
would be better than nothing.

Interestingly Felix supports that, and it is precisely
how typeclasses passed to functions are implemented:

	fun f[t with Eq[t]] (a:t, b:t, c:t) =>
		a < b and b < c
	;

	// same as "f: Eq t => t :: t * t -> t" in Haskell?

is actually implemented by

		open Eq[t];
		return a < b and b < c;

So in Ocaml if you could also "pass" in the module to be
opened it would be really cool! This should not require
properly first class modules: Felix does it without
them so Ocaml could too :)

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

Re: [Caml-list] Polymorphic Variants

[Tom]

[-- Attachment #1: Type: text/plain, Size: 2342 bytes --]

> Both reasons have practical impact. For the first one, using erasure
> semantics means that the programmer also can discard types when
> understanding the runtime behaviour of a program.


Actually, what I had in mind is exclusivelly compile-time overloading, which
causes no overheed at runtime.




> > Hm... Actually, what I had in mind is nominal subtyping... similar to
> > objects, in fact, objects in C++-like languages, just that they have no
> > class methods.
>
> Reading the description below, this all looks nice, independently of
> the semantics limitation described above. However, you can kiss
> farewell to type inference. With such an extensive overloading, you
> would need type annotations all over the place.
>

For the second one,
> you can write code that is maximally polymorphic, without too much
> fear about the impact of performance (equality is overloaded, so
> it still matters...) or strange ambiguity-related error messages.



I believe that "strange ambiguity-related error messages" are the result of
stupid programmers, not of the language. If one is careful to design a sane
library, most ambiguities never happen! Besides, incorporating whole-program
analysis (in the spirit of MLton), one can postpone such errors until the
whole application has been written, so for example local ambiguities would
be resolved by examining the uses (if a function is always called with
arguments of single type, there is no ambiguity).


> Not for records, but for objects. From a type-theoretic point of view
> they are just equivalent.





> By the way, this all looks likes the "used this feature in C++"
> syndrome. Sure C++ is incredibly powerful. But it is built on rather
> shaky theoretical fundations. So you can't expect to bring everything
> from C++ to a new language. Why not think about new ways to solve
> problems :-)


Well, I am... but just as you are in your message mentioning the practical
impact, so am I. And I think that every way to implement subtyping of
records/objects (=named tuples) other than the C++ way has an important
practical consequence - it's just slow. I guess that C++ like index-based
access is much faster than name-based access neccessary for structural
subtyping. Thou, please prove me that I am wrong :) I want structural
subtyping, the OCaml way, just very fast.

- Tom

[-- Attachment #2: Type: text/html, Size: 3310 bytes --]

[Caml-list] Polymorphic variants

[John Max Skaller]

I've been using polymorphic variants for a little while, and am
interested in their current status. Here are some comments. The 
executive summary is:
they're definitely worth using, and definitely worth continued
development.

My project is a compiler. The main reason I switched to
polymorphic variants is that term desugaring and reductions
would appear to be best handled by a single large term type,
and a various subsets appropriate to context. For example,
a type expression is a subset of an expression: it admits
addition, multiplication and exponentiation, but no
subtraction.

Unfortunately, this doesn't work out as well as I'd expected
because of recursion:

type a = [`A of a  | `B]
type b = [`A of  b]

The second type is a subtype of the first,
but this fails:

let f (x:a) =
match x with
  #b -> ()

with the message:

This pattern matches values of type [< b] = [< `A of b]
but is here used to match values of type a = [ `A of a | `B];;

Ocaml understands subtyping by subsets of variants,
but the constructor arguments must be invariant.
The work around is to decode the argument manually,
but then one wonders what the gain over standard variants is.
Here is another example:

 type x = [`A of int | `A of float];;
This variant type contains a constructor [ `A of float] which should be
[ `A of int]

No, I meant what I said! I can write both:

`A 1

and also

`A 1.1

and I am trying  to tell the compiler they both belong
to type x. It has no right to complain here. Of course,
this does lead to a problem:

 match x with | `A a -> ..

what type is a? It's 'a initially,
and bound on the first use. Which makes
matching on first `A 1 and then `A 1.1
impossible.  This is a problem with the ocaml type
inference mechanism not my type declaration!
[So it can't deduce the type of a .. but I could specify it
if there were syntax like

| `A (a:int) -> ...

[It seems to me that the type of the argument
is taken *incorrectly* as the intersection
type int & float, when it is actually a sum..
in the case of a sum the constraint would be
enough to fix the type correctly .. on the other hand,
intersections would correctly solve the covariance
problem .. ??]

In fact I found the type inference
engine stumbled around over legitimate matches,
and some extra help in the form of function argument
type  constraints was necessary (a small price to pay,
but worth noting an example in the manual).

In any case, polymorphic variant constructors really
ARE overloaded, but when it comes to declaring
types, overloading isn't allowed. This is an anomaly ..
and it hit me quite hard initially, because of the natural
attempt to try to use covariant arguments.

A second problem I found is the verbose error messages.
When you have 20 variants, a mismatch is a real pain
to decypher. It would be useful if variants HAD to be
declared like:

variant `A of int
variant `A of float
variant `B of long

so that spelling mistakes and type errors in constructor
arguments could be more easily pinpointed .. but of course,
this can't work due to recursion ... hmmm...

One thing that *definitely* needed improvement is the syntax
for declaring types: having to repeat all the cases every time
is an error prone tedium. It appears this HAS been done in
ocaml 3.04! THANK YOU!! One can now write:

type a = [`A]
type b = [`B]
type c = [a | b]

[#types were previously allowed in pattern matches but not
type declarations ..]

Well, are polymorphic variants worth the effort?
I think they are: they're not perfect, they're certainly
more error prone than standard variants .. but they're
also a lot more expressive and save considerable
coding, and in many cases they're much faster as well.
[In particular, injecting a subset of cases into a supertype
is a no-operation, whereas standard variants require
actually building new values]


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

[Remi VANICAT]

John Max Skaller <skaller@ozemail.com.au> writes:

> Unfortunately, this doesn't work out as well as I'd expected
> because of recursion:
> 
> type a = [`A of a  | `B]
> type b = [`A of  b]
> 
> The second type is a subtype of the first,
> but this fails:
> 
> let f (x:a) =
> match x with
>   #b -> ()
> 
> with the message:
> 
> This pattern matches values of type [< b] = [< `A of b]
> but is here used to match values of type a = [ `A of a | `B];;


the problem here is that you intended #b is a non fixed matching rule,
I mean, imagine you have :

`A (`A ( `A ( `A ( `A ( `A `B)))))

to check that this is not in #b, one have to look deep in the
structure of the value. pattern matching only look at the firsts
levels of the structure. This must be done otherwise. for example :

type a = [`A of a | `B | `C]
type b = [`A of b | `C]

let rec f (x:a) =
  match x with
  | `A x -> `A (f x)
  | `C -> `C
  | _ -> failwith "arg";;

> 
> Ocaml understands subtyping by subsets of variants,
> but the constructor arguments must be invariant.
> The work around is to decode the argument manually,
> but then one wonders what the gain over standard variants is.
> Here is another example:
> 
>  type x = [`A of int | `A of float];;
> This variant type contains a constructor [ `A of float] which should be
> [ `A of int]
> 
> No, I meant what I said! I can write both:
> 
> `A 1
> 
> and also
> 
> `A 1.1

No, you can't. the types informations are lost at runtime, so ocaml
will never be able to make the difference between the two.

> 
> and I am trying  to tell the compiler they both belong
> to type x. It has no right to complain here. Of course,
> this does lead to a problem:
> 
>  match x with | `A a -> ..
> 
> what type is a? It's 'a initially,
> and bound on the first use. Which makes
> matching on first `A 1 and then `A 1.1
> impossible.  

it won't be enough, to fail to match this, ocaml should be able to
know type at runtime. Type doesn't not exist at runtime

> This is a problem with the ocaml type
> inference mechanism not my type declaration!
> [So it can't deduce the type of a .. but I could specify it
> if there were syntax like
> 
> | `A (a:int) -> ...
> 
> [It seems to me that the type of the argument
> is taken *incorrectly* as the intersection
> type int & float, when it is actually a sum..
> in the case of a sum the constraint would be
> enough to fix the type correctly .. on the other hand,
> intersections would correctly solve the covariance
> problem .. ??]
> 
> In fact I found the type inference
> engine stumbled around over legitimate matches,
> and some extra help in the form of function argument
> type  constraints was necessary (a small price to pay,
> but worth noting an example in the manual).
> 
> In any case, polymorphic variant constructors really
> ARE overloaded, but when it comes to declaring
> types, overloading isn't allowed. This is an anomaly ..
> and it hit me quite hard initially, because of the natural
> attempt to try to use covariant arguments.
> 
> A second problem I found is the verbose error messages.
> When you have 20 variants, a mismatch is a real pain
> to decypher. It would be useful if variants HAD to be
> declared like:
> 
> variant `A of int
> variant `A of float
> variant `B of long
> 
> so that spelling mistakes and type errors in constructor
> arguments could be more easily pinpointed .. but of course,
> this can't work due to recursion ... hmmm...
> 
> One thing that *definitely* needed improvement is the syntax
> for declaring types: having to repeat all the cases every time
> is an error prone tedium. It appears this HAS been done in
> ocaml 3.04! THANK YOU!! One can now write:
> 
> type a = [`A]
> type b = [`B]
> type c = [a | b]
> 
> [#types were previously allowed in pattern matches 

it's not type in pattern matching, it's pattern. It is not, at all,
the same thing, even if their is link between the two.

> but not type declarations ..]

not exactly :


type foo = [ 'BAR ]
type 'a t = 'a constraint 'a = #foo;;

is correct, but deprecated, one should use :

type 'a t = 'a constraint [< foo] = 'a;;

> 
> Well, are polymorphic variants worth the effort?
> I think they are: they're not perfect, they're certainly
> more error prone than standard variants .. but they're
> also a lot more expressive and save considerable
> coding, and in many cases they're much faster as well.
> [In particular, injecting a subset of cases into a supertype
> is a no-operation, whereas standard variants require
> actually building new values]

You should look to the mixin.ml file that can be found in testlabl
directories of the source distribution, it show how to make what you
seem to want.
-- 
Rémi Vanicat
vanicat@labri.u-bordeaux.fr
http://dept-info.labri.u-bordeaux.fr/~vanicat
-------------------
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

[John Max Skaller]

Remi VANICAT wrote:

>John Max Skaller <skaller@ozemail.com.au> writes:
>
>>Unfortunately, this doesn't work out as well as I'd expected
>>because of recursion:
>>
>>type a = [`A of a  | `B]
>>type b = [`A of  b]
>>
>>The second type is a subtype of the first,
>>but this fails:
>>
>>let f (x:a) =
>>match x with
>>  #b -> ()
>>
>>with the message:
>>
>>This pattern matches values of type [< b] = [< `A of b]
>>but is here used to match values of type a = [ `A of a | `B];;
>>
>
>the problem here is that you intended #b is a non fixed matching rule,
>I mean, imagine you have :
>
>`A (`A ( `A ( `A ( `A ( `A `B)))))
>
>to check that this is not in #b, one have to look deep in the
>structure of the value. 
>
Yes. But high level programming languages are *meant* to do
high level things, aren't they?

Here's another example that fails, which is very annoying:

type a = [`A of e | `B]
and e = [a  | `C]

"The type constructor a is not yet completely defined"

Arggg. Of course it isn't. It works just fine if I textually
substitute:

type a =[`A of e | `B]
and e = [`A of e|`B|`C]

Almost all interesting cases of variants (for compiler writers anyhow)
involve type recursion. It shouldn't matter if the type is completely
defined, only that the definition is finally completed :)

BTW: I can't write  "t as x" in a type expression. Why not?
I'm forced to name it in a type binding .. that means that inductive types,
for example, can not be specified anonymously:

  (Cons of list | Empty) as list

Yeah, ocaml sum types are generative ... but the polymorphic
variant equivalents are not .. so

  [`Cons of list | `Empty] as list

should work. [Can I use a 'constraint' here? I've never used
a constraint before]

>pattern matching only look at the firsts
>levels of the structure. This must be done otherwise.
>
It doesn't "must" be done. I think you mean, there are advantages
only handling the easy cases: easy to write the compiler,
easy to optimise, easy for the end user to monitor
code complexity .. and easy for the programmer to handle
the more difficult cases manually ..

> for example :
>
>type a = [`A of a | `B | `C]
>type b = [`A of b | `C]
>
>let rec f (x:a) =
>  match x with
>  | `A x -> `A (f x)
>  | `C -> `C
>  | _ -> failwith "arg";;
>

The compiler doesn't know the type of x here,
at least without looking at the usage (clearly, usage
dictates type a). But the ambiguity could easily
be resolved by the client with an annotation.

>>
>>No, I meant what I said! I can write both:
>>
>>`A 1
>>
>>and also
>>
>>`A 1.1
>>
>
>No, you can't. the types informations are lost at runtime, so ocaml
>will never be able to make the difference between the two.
>
I certainly can write them both:

`A 1; `A 1.1;
type int_t = [`A of int];
type float_t = [`A of float];;

No problem doing this. Perhaps there should be.
The problem only manifests here:

type num = [ int_t | float_t ]

because the same constructor name has two different
argument types. It is even possible to write a function
that accepts both

let f x = x

happily accepts both :-)

Now you say that the type information is lost at run time,
but that is NOT immediately apparent from the documentation.
Indeed, it need not be the case: the implementation *could*
mangle the constructor name with the argument type
so that

  `A_int
  `A_float

are treated as distinct constructors. Then the following:

fun x = match x with
| `A a -> ..

would give an error, since the compiler cannot know
which `A it is, however the problem could easily be fixed
by the user:

| `A (a:int) ->

now we know it is `A of int. Things "must be so"
if they are a consequence of theory, but it isn't
always evident which theory is used, and why that
one is best :-)

Perhaps one consequence of this is that the documentation
needs to be more specific and have more examples:
the author knowing the chosen theory and implementation
believes only lightweight coverage is necessary, not seeing
the many alternatives someone less involved might.

For example, C++ objects DO have associated and accessible
run time type information. I know Ocaml doesn't .. but there are
other things I know less well, and there are C++ users
coming to ocaml that might think pattern matching
uses RTTI.

To come back to the examples: the type

[`A of int | `A of float | `B]

is perfectly legitimate. The actual error is only on matching.
If the client never matches on `A, there is no error:

match x with | `B -> .. | _ -> ...

this match would be OK, `A isn't refered to.
It isn't clear why the compiler writer chose to allow
any argument of `A, but disallows specifying a name for
a type containing two distinct `A constructors instead
of simply reporting an ambiguity on use: they're
called "polymorphic variants" but they aren't actually polymorphic,
at least in this sense :-)


>
>it's not type in pattern matching, it's pattern. It is not, at all,
>the same thing, even if their is link between the two.
>
Sure, I know that. (Actually, the sum constructor tags really ARE
run time type information, they tell which case of the sum
is represented, and hence the type of the constructor argument)

>
>You should look to the mixin.ml file that can be found in testlabl
>directories of the source distribution, it show how to make what you
>seem to want.
>
The biggest problem I have with ocaml, is that while I can
make anything I want, it is often not evident just what the
compiler/language permits, and what it doesn't.

This is particularly serious for me when it comes to modules:
it just isn't clear to me what will work and what will not,
and experiments here can be very time consuming and laborious.
The ideas seem simple, but the syntax is sometimes quite arcane,
and all sorts of restrictions that don't exist in the underlying
basic category theory can bite you days into a project.

To give a more concrete example: the first time I tried to
use polymorphic variants, I lost a week and had to undo
all my changes because I kept getting error messages I
couldn't make head or tail of. I decided to try again
when my project got even more complex, and I really needed
stronger static typing, but didn't want to create a huge number
of standard sum types and laboriously code the maps between
them case by case .. not to mention the industrial requirement
that every type have an associated print routine, for example.

I pressed on despite the horrendous error messages,
knowing that the transormation HAD to be totally
mechanical in the first instance. [Replace A with `A ..]

I lost another week due to a bug in Ocaml 3.02.
It took a while to determine this really was a compiler bug
matching polymorphic variants (3.01 worked fine,
and so does 3.04).

[My point is that it is very hard to proceed when you don't
know if an error is a bug in your understanding, a bug
in your implementation, or a bug in the compiler ..
so it is safer to eliminate the first case by not using
advanced features .. but if this argument were extended,
it would be an argument for using C instead of ocaml...]

Well, having looked at the English translation of the 
Ocaml book by Emmanuel Chailloux, Pascal
Manoury and Bruno Pagano, I think a big hole is going
to be plugged. This book covers quite advanced topics,
I might learn something here!

Anyhow .. sadly, ocaml is such a wonderful language.
I say sadly because I am unemployed and poor .. and
just can't bring myself to work with C/C++ again.
Its just too much of a step backwards, and I'm not
enough of a diplomat to hide it from my fellow
workers or employers (who still think OO and C++
are wonderful, and Java is Gods own language ..)

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

[Jacques Garrigue]

From: John Max Skaller <skaller@ozemail.com.au>
> Remi VANICAT wrote:
> 
> >John Max Skaller <skaller@ozemail.com.au> writes:
> >
> >>Unfortunately, this doesn't work out as well as I'd expected
> >>because of recursion:
> >>
> >>type a = [`A of a  | `B]
> >>type b = [`A of  b]
> >>
> >>The second type is a subtype of the first,
> >>but this fails:
> >>
> >>let f (x:a) =
> >>match x with
> >>  #b -> ()
> >>
> >>with the message:
> >>
> >>This pattern matches values of type [< b] = [< `A of b]
> >>but is here used to match values of type a = [ `A of a | `B];;
> >>
> >
> >the problem here is that you intended #b is a non fixed matching rule,
> >I mean, imagine you have :
> >
> >`A (`A ( `A ( `A ( `A ( `A `B)))))
> >
> >to check that this is not in #b, one have to look deep in the
> >structure of the value. 
> >
> Yes. But high level programming languages are *meant* to do
> high level things, aren't they?

The only problem is that you're asking for potentially non-terminating
computation to be done during pattern-matching. No, Caml is not
Haskell.
By the way, you can of course do that with a when clause.
Unfortunately, if you want to coerce the value to be a "b", this will
force you to rebuild your value, but anyway you have to access all
leaves of your value before knowing whether it is actually a "b" or
not.
Note that it might be simpler to have most of your functions defined
for "a" rather than for "b", and coerce from "b" to "a":
  (_ : b :> a)
Note the double coercion here, (_ :> a) wouldn't work.

> Here's another example that fails, which is very annoying:
> 
> type a = [`A of e | `B]
> and e = [a  | `C]
> 
> "The type constructor a is not yet completely defined"

But your example is not recursive.
You can just write
  type e = [a | `C]
and it will work fine.

> Almost all interesting cases of variants (for compiler writers anyhow)
> involve type recursion. It shouldn't matter if the type is completely
> defined, only that the definition is finally completed :)

Yes, it matters. Because a variant is a flat type, and the definition
of a variant type depends on the definition of its parts.
Of course it would be possible to do a topological sort to search where
there is no recursion, and remove the recursion automatically.
But this doesn't seem to be the ML approach for values either, and it
wouldn't add any expressive power.

> BTW: I can't write  "t as x" in a type expression. Why not?
> I'm forced to name it in a type binding .. that means that inductive types,
> for example, can not be specified anonymously:
>
>   [`Cons of list | `Empty] as list
> 
> should work. [Can I use a 'constraint' here? I've never used
> a constraint before]

Yes you can. Wasn't it in the tutorial:

    [`Cons of 'list | `Empty] as 'list

> >pattern matching only look at the firsts
> >levels of the structure. This must be done otherwise.
> >
> It doesn't "must" be done. I think you mean, there are advantages
> only handling the easy cases: easy to write the compiler,
> easy to optimise, easy for the end user to monitor
> code complexity .. and easy for the programmer to handle
> the more difficult cases manually ..

Not only that: easily understandable properties. This is the most
important part.

> I certainly can write them both:
> 
> `A 1; `A 1.1;
> type int_t = [`A of int];
> type float_t = [`A of float];;
> 
> No problem doing this. Perhaps there should be.

There is no problem as long as these cases are used independently.
But you cannot mix them in the same variant type.
How are we going to build a model of [`A of int | `A of float].
Basically this suppose that we are able to build the union set of
ints and floats. All the type theory theory of ML is based on the fact
that there is no such set/type.

> Now you say that the type information is lost at run time,
> but that is NOT immediately apparent from the documentation.
> Indeed, it need not be the case: the implementation *could*
> mangle the constructor name with the argument type
> so that
> 
>   `A_int
>   `A_float
> 
> are treated as distinct constructors. Then the following:
> 
> fun x = match x with
> | `A a -> ..
> 
> would give an error, since the compiler cannot know
> which `A it is

What this basically means is that any use of `A without type
annotation should generate an error. The whole point of polymorphic
variants being that they are independent from definitions, I really
cannot follow you here.

Sorry, but the feature you are asking for is not polymorphic variants.
This looks more like tree automata types, like they have for XML
typing. This indeed allows for all strange inclusions and unions, but
you can forget about type inference. These are interesting for
themselves, but how to mix them with languages with type inference is
still an open problem.

> Things "must be so" if they are a consequence of theory, but it
> isn't always evident which theory is used, and why that one is best
> :-)

Read the papers :-)
There is a whole literature about lambda-calculus, type systems,
models...
One trouble is that it is hard to explain all this theory in a few
lines.

> Perhaps one consequence of this is that the documentation
> needs to be more specific and have more examples:
> the author knowing the chosen theory and implementation
> believes only lightweight coverage is necessary, not seeing
> the many alternatives someone less involved might.

You're probably right. But your remark also describes the basic
problem: as long as the author is the only one to document a feature,
his description will only be partial.

> To come back to the examples: the type
> 
> [`A of int | `A of float | `B]
> 
> is perfectly legitimate. The actual error is only on matching.
> If the client never matches on `A, there is no error:
> 
> match x with | `B -> .. | _ -> ...
> 
> this match would be OK, `A isn't refered to.
> It isn't clear why the compiler writer chose to allow
> any argument of `A, but disallows specifying a name for
> a type containing two distinct `A constructors instead
> of simply reporting an ambiguity on use: they're
> called "polymorphic variants" but they aren't actually polymorphic,
> at least in this sense :-)

Polymorphism being a subtle thing...
The polymorphism in variants only describes the fact they can be built
from a bunch of constraints, rather than being defined in advance.

Also, the type you are talking about is

  [< `A of int | `A of float | `B]

which is perfectly legitimate (in the current theory).
You can even name it:

  type 'a t = 'a constraint 'a = [< `A of int | `A of float | `B]

This type being polymorphic, you need to leave a variable to expose
this polymorphism.

On the other hand,
  [`A of int | `A of float | `B]
is the intersection of the above type and
  [> `A of int | `A of float | `B]
This last type is illegal, because you wouldn't be able to match such
a type.

Note that one could think of ways to make the above legal, using
intersection rather than union, but I don't see how it would be
useful, because you would have no way to access the value anyway.
Like throwing data into a black hole.

> >it's not type in pattern matching, it's pattern. It is not, at all,
> >the same thing, even if their is link between the two.
> >
> Sure, I know that. (Actually, the sum constructor tags really ARE
> run time type information, they tell which case of the sum
> is represented, and hence the type of the constructor argument)

They tell more: you may have several cases with the same type.

> Well, having looked at the English translation of the 
> Ocaml book by Emmanuel Chailloux, Pascal
> Manoury and Bruno Pagano, I think a big hole is going
> to be plugged. This book covers quite advanced topics,
> I might learn something here!

This is indeed a nice book, but written before the introduction of
polymorphic variants. So almost nothing about them in it.

Actually, this is one reason I would want to say: now polymorphic
variants are finished, let's work with them, and try to describe what
they can do. This is too hard to do that on a moving target.

Cheers,

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

[John Max Skaller]

Jacques Garrigue wrote:

>>BTW: I can't write  "t as x" in a type expression. Why not?
>>I'm forced to name it in a type binding .. that means that inductive types,
>>for example, can not be specified anonymously:
>>
>>  [`Cons of list | `Empty] as list
>>
>>should work. [Can I use a 'constraint' here? I've never used
>>a constraint before]
>>
>
>Yes you can. Wasn't it in the tutorial:
>
>    [`Cons of 'list | `Empty] as 'list
>
Argg. Sorry. Of course, I used a plain identifier instead of a type 
variable.

>>It doesn't "must" be done. I think you mean, there are advantages
>>only handling the easy cases: easy to write the compiler,
>>easy to optimise, easy for the end user to monitor
>>code complexity .. and easy for the programmer to handle
>>the more difficult cases manually ..
>>
>
>Not only that: easily understandable properties. This is the most
>important part.
>
Yes, but it is an amorphous thing. The specification
of an 'integer' is easily understandable. Only, the greatest
minds in mathematics struggle to know what a prime
number is.

>>I certainly can write them both:
>>
>>`A 1; `A 1.1;
>>type int_t = [`A of int];
>>type float_t = [`A of float];;
>>
>>No problem doing this. Perhaps there should be.
>>
>
>There is no problem as long as these cases are used independently.
>But you cannot mix them in the same variant type.
>
Yeah, I know .. but it isn't clear from the manual,
perhaps because this very example is not included in it.

>
>How are we going to build a model of [`A of int | `A of float].
>Basically this suppose that we are able to build the union set of
>ints and floats. All the type theory theory of ML is based on the fact
>that there is no such set/type.
>
Not at all. Felix does this, just fine. And I'm no type theorist.
But the algorithms work. I'm not saying ocaml should do
what I did in Felix, but there is no problem at all building
a model, `A is just a function, and in Felix functions
can be overloaded. Including variant constructors.
[These are classic ML style unions, not open ones
like polymorphic variants: they have to be declared
or it wouldn't work]

In Felix, it is fine to duplicate not just constructors,
but any function type:

fun f:x->y = ..
fun f:x->y= ..

No problem. But here:

print (f x);

there is a problem: which f to use?

Is this a good design decision? I don't know: I *could*
report a duplicate definition (and I *do* for duplicate
things other than than functions).

But there is evidence that this IS a good design
decision, it comes from overloading templates
in C++. Since a template basically models a family
of functions, two tempates often model the same
type .. and it would be really silly to ban the templates
because of this. Instead, an error is reported only
when a particular instantiation is ambiguous.

I'm not criticizing the decisions made for polymorphic
variants, just pointing out that a lot of alternatives
do exist, and it would be useful to see an explanation
of why the various interesting nasty cases are
handled the way they are.

>
>What this basically means is that any use of `A without type
>annotation should generate an error. The whole point of polymorphic
>variants being that they are independent from definitions, I really
>cannot follow you here.
>
Nor I you. When the compiler sees:

    `A 1

in an expression then it silently replaces it with


    `A_int 1

so that the actual constructor name is distinct for every argument type.
This is called 'name mangling' and C++ compilers do it all the time
to every external function symbol in a program.

In a pattern match, there is a problem because the mangling
cannot be done when the expression being decoded
is of a type with two constructor of the same unmangled name.
So in this case ONLY, the client must disambiguate by
specifying which type is meant:

    `A (x:int)


is replaced by

  `A_int x

>
>Sorry, but the feature you are asking for is not polymorphic variants.
>

I am NOT asking for it. I am merely critiquing it from the point
of view of a user. Remember, I am using them: the whole of my
compiler uses polymorphic variants extensively and almost
exclusively (only a few of the traditional sum types remain
in a couple of places because there is no point replacing them).
So you could say I'm a fairly heavy user of them :-)

>>Things "must be so" if they are a consequence of theory, but it
>>isn't always evident which theory is used, and why that one is best
>>:-)
>>
>
>Read the papers :-)
>There is a whole literature about lambda-calculus, type systems,
>models...
>One trouble is that it is hard to explain all this theory in a few
>lines.
>
And the other is that there are a LOT of theories.

Furthermore, the theory upon which an implementation
is based doesn't determine all the technical design decisions:
like, for example, whether to report that a type with duplicate
constructors is an error even if it isn't used, or whether
to defer the error to the point of use .. and provide a disambiguation
mechanism.

C++ for example, adopts BOTH of these philosophies in different
places, which is one reason it is a mess.

>>Perhaps one consequence of this is that the documentation
>>needs to be more specific and have more examples:
>>the author knowing the chosen theory and implementation
>>believes only lightweight coverage is necessary, not seeing
>>the many alternatives someone less involved might.
>>
>
>You're probably right. But your remark also describes the basic
>problem: as long as the author is the only one to document a feature,
>his description will only be partial.
>
So add in the example I gave? I can't do that, I don't have access to the
document source. But I have 'documented' it in the email :-)

>
>Note that one could think of ways to make the above legal, using
>intersection rather than union, but I don't see how it would be
>useful, because you would have no way to access the value anyway.
>Like throwing data into a black hole.
>
The pragmatics of programming often require useless things.
For example, unreachable code .. because the programmer
has commented something out. Empty types (why was []
removed??) because they're yet to be filled in with cases,
but we want to name the type anyhow, perhaps to write
a function signature ..

The unit type. It is theoretically useless in a (purely) functional
programming language. Why is it there?

>>Well, having looked at the English translation of the 
>>Ocaml book by Emmanuel Chailloux, Pascal
>>Manoury and Bruno Pagano, I think a big hole is going
>>to be plugged. This book covers quite advanced topics,
>>I might learn something here!
>>
>
>This is indeed a nice book, but written before the introduction of
>polymorphic variants. So almost nothing about them in it.
>
>Actually, this is one reason I would want to say: now polymorphic
>variants are finished, let's work with them, and try to describe what
>they can do. This is too hard to do that on a moving target.
>

Well, I'm doing my part: I'm using them all the time,
and I'm relating my experience so you can get some feeling
for how someone else views them that is. I was hoping
to get much stronger static typing using them. In fact,
I have better typing, but nowhere near as strong as I
either expected initially, or would like.

Some of the typing I'd like is plain impossible.
And some is inconvenient to implement, or too quirky
to bother with. And some is desirable but not implemented
or not understood. And I don't really know the distinction
between all these cases.

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