On Sep 7, 2006, at 12:20 PM, skaller wrote: >> I agree: the implementation of Type Classes is weak and currently >> does not take the concept far enough but I think you should learn >> Haskell and use type classes in a serious way before likening them to >> object-oriented programming. > > I would love to learn and use more Haskell .. but of course > there is are constraints: time is one, the need to depend on > tools readily available and easy to install on target platforms > is another, and the need for the system to run fast another.
Granted, Haskell isn't always fast but it is easier to express high level concepts in it and Felix is a compiler--on very large projects speed might matter but generally (maybe this is my own opinion) the resulting code is what counts. GHC actually runs on every platform Felix runs on (currently), except that GHC uses minGW and not cygwin; yhc needs a little more library support and it produces bytecodes; nhc98 would restrict you to using pretty much haskell98 (i.e., no GADT's) but Template Haskell, Arrows and other things are readily available as libraries. This may simply be academic--no sense changing horses in mid-stream. > Typeclasses identify the notion of 'kind' with 'typeclass' the > same way run time OO identifies the notion of 'type' with 'class'. That is actually well put but I'm not sure what you mean by 'kind'. In Haskell, 'kinds' are the type of types, for example the type of Int is *, that is (Int :: *); constructors have type (* -> *)-- depending on the implementation the * is may be an existential relation (otherwise the kind of a type would be unbounded). In Felix, kinds seem to be a mapping from one type to another (* -> *). Is this correct? Anyway, because an Algebraic Type may be declared toward a primitive type (type :: *), such as data NewInt = N Int -- (Int :: *), (N :: Int -> NewInt), (NewInt :: Int) where Int may be characterised as a 'kind', the distinction between 'kinds' and 'types' is gone as of GHC 6.6 and the System F type system: they are the same thing (to the intermediate-language type system, see http://hackage.haskell.org/trac/ghc/wiki/ IntermediateTypes). If that is your meaning of 'kind,' then no, type classes certainly do not work that way--type classes do not create 'kinds' or any sort of boundaries for types--that is, they have no direct effect on types. This is *not* the same thing as functors in ML/OCaml, which are bound certain types. An example would make this clearer: class Eq a where (==), (/=) :: a -> a -> Bool instance Eq a where x == y = not (x /= y) x /= y = not (x == y) I could still define equality over a type, without defining my type as an instance of Eq, except that the functions (==) and (/=) would not be available to me because--like all functions in Haskell--they are monomorphic except as defined within the class Eq. It would be the same problem as defining operator== in a C++ class. So I could define, say, isNewIntEq :: NewInt -> NewInt -> Bool isNewIntEq x y = if (x - y) then False else True or I could define my new type to be an instance of Eq so I could use the polymorphic version of the function (==): instance Eq NewInt where x == y = (x - y == 0) x /= y = not (x == y) Note: this is a bit contrived since NewInt is really a primitive type, but you get the point. > It isn't the subtyping of values (types) which is the issue, > but the subclassing of typeclasses (kinds). Subclassing type classes is a bit different than deriving functors or C++ classes. Subclassing type classes only really manages whether my types may take the (now more strictly parameterised) polymorphic functions. (Don't be confused: the function f :: forall a. => a -> a is parameterised over the monomorphic type 'a'.)For example: -- another contrived example class Eq a => Ord a where ... The (=>) is meant to emulate the logic symbol 'is an element of,' albeit backwards (right to left). For the contrived 'NewInt' type, an instance of Ord would include an instance of Eq: if I defined a function limited to an instance of Ord that would include types limited to instances of Eq but not vice versa: orderedT :: (Ord a) => a -> a --if I applied orderedT to a NewInt without defining NewInt as an instance of Ord, I would get a compile-time error here. > Sorry I can't explain this better .. but your example muddles > the 'levels' up: subtyping relations in wxWidgets are about > the relations of execution time values as abbreviated by > the notion of a class, which is a compile time value. Good distinction but I think it is less clear with the above example of type classes. > The problem with typeclasses is the same one level up: > the covariance problem for types/classes must exhibit > for kinds/typeclasses for the same reason: encapsulating > notions of types as properties of the types is entirely > wrong. Types do not have properties. They do not have > any structure at all. As above, type classes encapsulate the "polymorphism" of operations over types, not properties of types. I could define types perfectly well without type classes but it would be inconvenient without them. > It is the categories which define > the functions (arrows) operating on the types which > obey laws -- That is what type classes do, if you use them correctly. The above type class for Eq only defines the laws of the equality operations ( x == y = not (x /= y) and vice versa). I could use type classes to define commutativity, associativity, etc., as well. > expressed by equations between arrow compositions > in category theory -- which actually characterises a typing > system. Is ( x == y = not ( x /= y) ) an equation between arrow compositions? > The concept of 'abstract data type' is, quite simply, > entirely bogus because it implies such a thing is an abstract > view of a *single* type. Abstraction is precisely the arrows > and laws that govern them.. it is the CATEGORY which is the > type system .. the 'types' themselves are irrelevent points > with no properties or structure at all. That is the very > MEANING of abstraction, from a categorical viewpoint. I completely agree. Type classes are weak in that respect: there is no *necessary* connection between a type and a the 'laws' enforced by a type class; in practice, however, libraries have been build according to these type classes and so embody the laws. > Pure categories don't even have any objects: they're > merely a constructive convenience for our lame set theoretic > brains: an 'object' in a category is actually an identity > arrow. The class Eq a has no necessary objects--it simply operates over single elements of anything ( forall a ). > Now in ML, categories are not first class. That's the real > problem. Category theory treats 'higher order' categories > as 'just another category' and if you have three levels: > > category > functor > natural transformation > > you're done. The infinite hierarchy of concepts is done, > since category theory can now be applied to itself. That sounds neat. It seems like you would define a type as a member of a Category, over which you would have certain functions defined; it might be very constraining unless the compiler may automatically derive the actual functional operations over types. > This is why the 'pattern calculus' is important and implemented > in the type system, but not the executable patterns. That is exactly where it counts the most! This is the distinction between linguistic constructs and actual constructs: ultimately everything gets down to bits and pre-defined machine operations; Haskell, ML and many other languages have been compiled to C and still retained their operative nature. Whether it is a feature you want depends on whether programmers might find it useful operationally and even it is only linguistic. -Pete ------------------------------------------------------------------------- Using Tomcat but need to do more? Need to support web services, security? Get stuff done quickly with pre-integrated technology to make your job easier Download IBM WebSphere Application Server v.1.0.1 based on Apache Geronimo http://sel.as-us.falkag.net/sel?cmd=lnk&kid=120709&bid=263057&dat=121642 _______________________________________________ Felix-language mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/felix-language
