Ashley Yakeley:
I think existential types are arranged so that Haskell never needs to store type information in them at run-time. So you'll never be able to do dynamic OOP with them.
One possible extension to Haskell for dynamic OOP, which I never tire of suggesting, is the extensible datatype, for instance:
module P data BaseType = B1 | B2 | _
module Q data DerivedType = D1 | D2 data BaseType |= BD DerivedType
That rubs me the wrong way in that it invents new notions, eg, "| _" and "|=" when I get the feeling extant notions can be reused. Eg, why not try to replace the equality with an implication (both equality and implication being notions we already need to know), eg,
data BaseType <= B1 | B2
data BaseType <= D1 | D2
Of course, that is just an untested idea. My reason for posting is to bring attention to how something similar is done in the language merd, whose designer posts here under the name pixel, and which is actually implemented I think. Having just found this, I do not understand it, but it sure has the look, tone and feel of a good design. merd has a notation a !< b which means that values of type "a" can be used when expecting a value of type "b" --ie, it is a subtype. (note the similarity to "<=".) Haskell's data declaration makes a sum-of-products type, eg, data Maybe a=Nothing|Just a In contrast, merd has sum types written a|b and product types written (a,b) and data constructors which are capitalized, eg, True, Just. So this next is the definition of Maybe in merd: (Maybe,x) = Nothing | (Just,x) (I've simplified and renamed constructors a little.) I believe that factoring Haskell's datatypes into constituent parts, which merd does, is essential to a good subtyping design. Haskell's datatypes are too specialized for particular patterns of uses. In addition, merd has a type called a struct, written a |&| b. For reasons I do not understand, instead of defining, eg, point = (double,double) or point = (Point,double,double) pixel prefers to define point = (X,double) |&| (Y,double) That last way is the standard way of declaring a record type, says pixel. The fact that none of the types introduced so far can be built from the other 3 types is made clear by the rules for subtypes, some of which are (a0, ..., an) !< (b0, ..., bn) <=> ai !< bi (forall i) a !< a | b a |&| b !< a i !< a and i !< b <=> i !< a |&| b i !< a or i !< b <=> i !< a | b i !> a and i !> b <=> i !> a | b i !> a or i !> b <=> i !> a |&| b i !< a | b|&|c <=> i !< a|b |&| a|c i !> a |&| b|c <=> i !> a|&|b | a|&|c i !> i | a => i !> a i !< i | a => i !> a i !< i |&| a => i !< a i !> i |&| a => true i !> i|&|a | b => i !> b i !< i|a |&| b => i !> a and i !< b Oh, yeah, there is a function type of course --which obeys a|c->b !< a->b !< a->b|d A->B !> x->x <=> (exists x. A !< x and B !> x) The words "covariant" and "contravariant" are mentioned, whatever they are. More at http://cvs.sourceforge.net/cgi-bin/viewcvs.cgi/~checkout~/merd/ merd/subtyping.me?content-type=text/plain and http://merd.sourceforge.net/types.png
Richard Uhtenwoldt <greon@best.com> writes: [...]
My reason for posting is to bring attention to how something similar is done in the language merd, whose designer posts here under the name pixel, and which is actually implemented I think.
not really. still coding... :) [...]
Was in too small resolution, fixed. Try http://merd.sourceforge.net/types.pdf for nicer display.
In addition, merd has a type called a struct, written a |&| b. For reasons I do not understand, instead of defining, eg,
point = (double,double)
or
point = (Point,double,double)
pixel prefers to define
point = (X,double) |&| (Y,double)
The reason is tuples do not have any subtyping relationship (unless you add it, but it gets ugly ;p) (it also enforces that record fields are not ordered) The |&| is defined elsewhere[1] as /\ aka the intersection type operator (maybe i should rename it, |&| is ugly, /\ is not bad...) It is generally used as a record subtyping operator. It is also used for ad'hoc overloading: show !! String -> String |&| Int -> String [2] but in fact, it can be useful in many areas, if you allow |&| to work on values: default_val = 0 |&| [] [ 1, "foo" ].map(x -> x + 1|&|"bar") #=> [ 2, "foobar" ] - type of [ 1, "foo" ] is List(1 | "foo") (just like type of [ True, False ] is List(Bool) where Bool = True | False) - (x -> x + 1|&|"bar") is alike (x -> x + 1) |&| (x -> x + "bar") so the type is Int->Int |&| String->String [3] - the result is of type List(String | Int) [4] for pattern matching: "(\s+):(\d+)" returns String, String|&|Int allowing the use with no cast as an Int and/or as a String [1] Intersection Types and Bounded Polymorphism http://citeseer.nj.nec.com/54630.html [2] can be factorised as show !! String|Int -> String [3] well in fact + !! o,o -> o where o !< &Addable so the type is x -> x where 1|&|"bar" !< x !< &Addable which gives x -> x where x !< String|Int when going to the closed world where + is defined for types Int and String [4] hum, in fact merd evaluates what it can at compile time, so the type is the type of [ 2, "foobar" ] which is List(2 | "foobar") -- Pixel
participants (2)
-
Pixel -
Richard Uhtenwoldt