[Haskell-cafe] Haskell's type system compared to CLOS
Hi, usually I'm sceptical of programming languages which are not based on the von Neumann architecture, but recently I got interested in functional programming languages. The arrogance of lots of Haskell users, who made me feel that using a programming language other than Haskell is a waste of time, combined with vanguard mathematical notation has been very attractive to me and I have decided to get at least an idea of Haskell and its concepts. Some weeks ago I learned programming in Dylan and was impressed by its object system which is basically a stripped version of CLOS. Multiple dispatch together with a well-thought-out object system is quite powerful, because it removes the burden of including methods in the class definition. At the moment I'm reading the Functional Programming using Standard ML and I'm in the chapter on data types. This afternoon it occurred to me that classes and data types are symmetric. In a class hierarchy you start an abstract super class (the most abstract is the class object in some languages) and further specialise them via inheritance; with data types you can start with specialized versions and abstract them via constructors (I'm not sure how message sending to a superclass looks like in this analogy). Anyhow, I also came across an interesting presentation. Andreas Löh and Ralf Hinze state in their presentation Open data types and open functions [1]: * OO languages support extension of data, but not of functionality. * FP languages support extension of functionality, but not of data. Their first point refers to the fact that in most object-oriented languages don't allow the separate definition of classes and their respective methods. So to add new functions, you have edit the class definitions. However, in functional programming languages you can easily add new functionality via pattern matching, but have to either introduce new types or new constructors, which again means to modify existing code. In Dylan (and in Common Lisp) you define methods separate from classes and have pattern matching based on types. This solves all mentioned problems. So my question is, how are algebraic data types in Haskell superior to CLOS (despite the fact that CLOS is impure)? How do both compare? What has Haskell to provide what Common Lisp and Dylan haven't? Thanks! Regards, Matthias-Christian [1] http://people.cs.uu.nl/andres/open-japan.pdf ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell's type system compared to CLOS
Matthias-Christian Ott wrote: Hi, usually I'm sceptical of programming languages which are not based on the von Neumann architecture, but recently I got interested in functional programming languages. The arrogance of lots of Haskell users, who made me feel that using a programming language other than Haskell is a waste of time, combined with vanguard mathematical notation has been very attractive to me and I have decided to get at least an idea of Haskell and its concepts. Some weeks ago I learned programming in Dylan and was impressed by its object system which is basically a stripped version of CLOS. Multiple dispatch together with a well-thought-out object system is quite powerful, because it removes the burden of including methods in the class definition. At the moment I'm reading the Functional Programming using Standard ML and I'm in the chapter on data types. This afternoon it occurred to me that classes and data types are symmetric. In a class hierarchy you start an abstract super class (the most abstract is the class object in some languages) and further specialise them via inheritance; with data types you can start with specialized versions and abstract them via constructors (I'm not sure how message sending to a superclass looks like in this analogy). Anyhow, I also came across an interesting presentation. Andreas Löh and Ralf Hinze state in their presentation Open data types and open functions [1]: * OO languages support extension of data, but not of functionality. * FP languages support extension of functionality, but not of data. Their first point refers to the fact that in most object-oriented languages don't allow the separate definition of classes and their respective methods. So to add new functions, you have edit the class definitions. However, in functional programming languages you can easily add new functionality via pattern matching, but have to either introduce new types or new constructors, which again means to modify existing code. In Dylan (and in Common Lisp) you define methods separate from classes and have pattern matching based on types. This solves all mentioned problems. So my question is, how are algebraic data types in Haskell superior to CLOS (despite the fact that CLOS is impure)? How do both compare? What has Haskell to provide what Common Lisp and Dylan haven't? Thanks! Regards, Matthias-Christian Type classes. Mike ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell's type system compared to CLOS
On Tue, Aug 11, 2009 at 11:20:02PM +0100, Philippa Cowderoy wrote: Matthias-Christian Ott wrote: What has Haskell to provide what Common Lisp and Dylan haven't? Static typing (with inference). Very large difference, that. That's true. This is a big advantage when compiling programmes. But as far as I know type inference is not always decidable in Haskell. Am I right? Dylan does type inference too and Hannes Mehnert is currently working on better type inference for the dylan compiler [1]. Regards, Matthias-Christian [1] https://berlin.ccc.de/wiki/Dem_Compiler_beim_Optimieren_zuschauen ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell's type system compared to CLOS
Matthias-Christian Ott o...@mirix.org writes: That's true. This is a big advantage when compiling programmes. But as far as I know type inference is not always decidable in Haskell. Am I right? Decidability of type inference depends on features you use (GADTs, type classes etc). Type inference in Haskell doesn't mean you avoid providing type signatures at all costs. It is good programming practice to provide type signatures, as elaborate design of ADTs, type classes you use in your program gives you possibility to encode specification of how program behaves in static, that is type signatures help you to document your code. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell's type system
ronwalf: I'm trying to wrap my head around the theoretical aspects of haskell's type system. Is there a discussion of the topic separate from the language itself? Since I come from a rather logic-y background, I have this (far-fetched) hope that there is a translation from haskell's type syntax to first order logic (or an extension there-of). Is this done? Doable? A quick link to get you started on the topic, I'm sure others will add more material. Haskell's type system is based on System F, the polymorphic lambda calculus. By the Curry-Howard isomorphism, this corresponds to second-order logic. The GHC compiler itself implements Haskell and extensions by encoding them in System Fc internally, which extends System F with support for non-syntactic type equality.. JHC, I believe, encodes Haskell into a pure type system internally, some sort of higher order dependently-typed polymorphic lambda calculus. -- Don ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell's type system
On Tue, Jun 17, 2008 at 2:40 PM, Ron Alford [EMAIL PROTECTED] wrote: I'm trying to wrap my head around the theoretical aspects of haskell's type system. Is there a discussion of the topic separate from the language itself? Since I come from a rather logic-y background, I have this (far-fetched) hope that there is a translation from haskell's type syntax to first order logic (or an extension there-of). Is this done? Doable? Sort of, via the Curry-Howard Correspondence. Haskell's type system corresponds to a constructive logic (no law of excluded middle). Arbitrary quantifiers are also introduced via the RankNTypes (I think that's what it's called) extension. Haskell's type system is a straightforward polymorphic type system for the lambda calculus, so researching the Curry-Howard Correspondence will probably get you what you want. Luke ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell's type system
On Tue, Jun 17, 2008 at 04:40:51PM -0400, Ron Alford wrote: I'm trying to wrap my head around the theoretical aspects of haskell's type system. Is there a discussion of the topic separate from the language itself? Since I come from a rather logic-y background, I have this (far-fetched) hope that there is a translation from haskell's type syntax to first order logic (or an extension there-of). Is this done? Doable? I'll give you some terms to Google for. The ideal type system for Haskell (ignoring type classes) is System F. Haskell'98 doesn't quite get there, but recent extensions such as boxy types and FPH do. System F corresponds to second order propositional logic: types correspond to propositions in this logic, and Haskell programs as the corresponding proofs (by the Curry-Howard isomorphism). The type system of Haskell'98 is a bit weird from a logical perspective, and sort of corresponds to the rank 1.5 predicative fragment of second order propositional logic (I say rank 1.5 because although no abstraction over rank 1 types is allowed normally, limited abstractions over rank 1 types is allowed through let-polymorphism -- so this is *almost* first order logic but not quite: slightly more powerful). Regarding type classes, I'm not 100% what the logical equivalent is, although one can regard a type such as forall a. Eq a = a - a as requiring a proof (evidence) that equality on a is decidable. Where this sits formally as a logic I'm not sure though. Edsko ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell's type system
On Jun 17, 2008, at 11:08 PM, Don Stewart wrote: Haskell's type system is based on System F, the polymorphic lambda calculus. By the Curry-Howard isomorphism, this corresponds to second-order logic. just nitpicking a little this should read second-order propositional logic, right? daniel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell's type system
On 6/18/08, Edsko de Vries [EMAIL PROTECTED] wrote: Regarding type classes, I'm not 100% what the logical equivalent is, although one can regard a type such as forall a. Eq a = a - a as requiring a proof (evidence) that equality on a is decidable. Where this sits formally as a logic I'm not sure though. You can take the minimalist view and treat a typeclass parameter as an explicitly passed dictionary; that is: (Eq a = a - a) is isomorphic to (a - a - Bool, a - a - Bool) - a - a In fact, this is basically what GHC does. You then treat an instance declaration: instance Eq Int where (==) = eqInt# (/=) = neqInt# as just a constant Eq_Int = (eqInt#, neqInt#) -- ryan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Haskell's type system
I'm trying to wrap my head around the theoretical aspects of haskell's type system. Is there a discussion of the topic separate from the language itself? Since I come from a rather logic-y background, I have this (far-fetched) hope that there is a translation from haskell's type syntax to first order logic (or an extension there-of). Is this done? Doable? -Ron ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
