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