On Thu, 2006-09-07 at 11:11 -0400, Peter Tanski wrote: > On Sep 7, 2006, at 7:20 AM, skaller wrote: [] > Although having a type-checking system at runtime *may* require > runtime system support, you might implement it statically in the > final program but the simplification process and code generation > would become very complex.
Yes .. or no .. depending on the model chosen. The implementation technique is then an extra burden on top of understanding the theory being implemented .. which is why having theoreticians on the team is so essential. > I give > you all this information for a simple reason: Much as I would love to read every research paper ever written I think my brain would explode .. :) > yes, Felix is a > language for implementing recent research; however, Felix runs into > two problems: (1) the simple combination of all the different > research is itself research of a sort Yes indeed. > and (2) holding the line to > category theory as opposed to type theory may not seem that different > at a high level (they should ultimately describe the same thing) but > the implementation of each is different so you will inevitably course > into uncharted waters. Yes -- it would be no fun otherwise :) > You might make that easier on yourself by > doing a little translation of the previous explorations. (I say > "yourself," but I might be able to get involved in this with the > caveat that I would probably do the implementation in Haskell, not > OCaml.) I do try to do that, however there's one of me, acting entirely without funding, and without sufficient brain power or academic background, so I have to do what I can in a relative vaccuum. This does have some advantages .. being naive I happily implement things based on intuition instead of theory and sometimes find I'm ahead of the researchers. Often I have no real idea whether what I'm doing is 'obvious' or novel. Such a development process would be hopeless were it not for the fact that compilers are rigorous formal tools, so if I can actually get the Ocaml typing for some feature right there's a good chance the thing is actually a sound idea. > 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. Indeed, bootstrapping via GHC and using the FFI is very appealing compared to Ocaml. > At least read "From Hindley-Milner > Types to First-Class Structures," at http://web.cecs.pdx.edu/~mpj/ > pubs/haskwork95.pdf , which got the whole type classes thing started > but remember that whatever the genesis of type classes may have been > (essentially polymorphism), their use is somewhat different today. > For a good example of how type classes have *not* been used for > object-oriented hierarchies, I refer you to the implementation of > wxHaskell which uses type hierarchies (not type classes) to model the > object-oriented model of wxWidgets in Haskell: the documentation is > here http://wxhaskell.sourceforge.net/doc/. The issue here is not subtyping types, but subclassing typeclasses. The types are values of the system at compile time: the typeclasses are the issue here. Typeclasses identify the notion of 'kind' with 'typeclass' the same way run time OO identifies the notion of 'type' with 'class'. It isn't the subtyping of values (types) which is the issue, but the subclassing of typeclasses (kinds). 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. 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. It is the categories which define the functions (arrows) operating on the types which obey laws -- expressed by equations between arrow compositions in category theory -- which actually characterises a typing system. 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. 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. Translated to type *systems* any attempt to characterise types by properties is just wrong in principle. ML modules do not do this: a module has a set of types (objects) and functions (arrows). The module Map in Ocaml is NOT a type. Map.t is a type .. and so is Map.elt There are two types here .. and it is the relations between then expressed by the (unstated!) relations between the functions of the module which actually characterise the typing. Note: *typing* is the word, not type: a Map is not a type, its a category. 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. With ML modules/functors this isn't so. The model using modules and functors is correct and typeclasses are not. The problem is that these things can't be applied to themselves. This is why the 'pattern calculus' is important and implemented in the type system, but not the executable patterns. We don't really care about the final code generation stage of the reduction processes because it is heavily influence by the target language, be it C++ or assembler. It's the stages above that .. the type system .. which needs to have the 'infinite regress' removed by a kinding system which can be applied to itself. Pattern calculus looks good because it is self-applicative -- like lambda calculus -- but it covers 'deabstraction' as well as abstraction (in other words it allows calculation of patterns = destructors as well as constructors). -- John Skaller <skaller at users dot sf dot net> Felix, successor to C++: http://felix.sf.net ------------------------------------------------------------------------- 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
