Re: [Haskell-cafe] Monad.Reader 8: Haskell, the new C++
On Fri, 2007-09-14 at 21:55 +0200, Peter Verswyvelen wrote: > I'm not sure, I don't know LISP in detail, but as far as I know, LISP > is a fully dynamic language. > > I actually meant a static language where you build your own strong > types using the language itself. On the micro level, the language only > knows abouts bits and bytes without semantics, just like assembler, no > types at all. But the language allows you to build whatever "type" or > "semantics" you want from scratch, by providing a keyword that forces > certain part of the program to be evaluated at compile time. A bit > like macros, but written in the same language. Although not exactly > the same, the Digital Mars D language has a "static if (p) { q }" > statement, where p must evaluate to a constant expression at compile > time, otherwise the compiler gives an error/warning (I'm not sure, > haven't tried it yet). You can do that in C++ (using templates) and > Haskell (using types) but these are actually mini-sub-languages. > Probably giving control to the programmer of how type-checking should > be coded bypasses the advantages of strong typing, so this is most > likely a dumb idea... You might find Forth interesting/entertaining. After implementing versions of Dijkstra's guarded if and do constructs using the same mechanisms that were used to implement the "native" control structures I decided that Forth was the closest thing to a genuine extensible language that I had ever worked with. -- Bill Wood ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Monad.Reader 8: Haskell, the new C++
I'm not sure, I don't know LISP in detail, but as far as I know, LISP is a fully dynamic language. I actually meant a static language where you build your own strong types using the language itself. On the micro level, the language only knows abouts bits and bytes without semantics, just like assembler, no types at all. But the language allows you to build whatever "type" or "semantics" you want from scratch, by providing a keyword that forces certain part of the program to be evaluated at compile time. A bit like macros, but written in the same language. Although not exactly the same, the Digital Mars D language has a "static if (p) { q }" statement, where p must evaluate to a constant expression at compile time, otherwise the compiler gives an error/warning (I'm not sure, haven't tried it yet). You can do that in C++ (using templates) and Haskell (using types) but these are actually mini-sub-languages. Probably giving control to the programmer of how type-checking should be coded bypasses the advantages of strong typing, so this is most likely a dumb idea... Anyway, I should not mention these ideas, I'm just a programmer, not a computer scientist ;-) Peter Adrian Neumann wrote: -BEGIN PGP SIGNED MESSAGE- Hash: RIPEMD160 I heard only rumors, but isn't Lisp supposed to be just that? A programmable programming language? Peter Verswyvelen schrieb: This is all very cool stuff, but sometimes I wander if it isn't possible to drop the special languages for fiddling with types, and introduce just a single language which has no types, only raw data from which you can built your own "types" (as in the old days when we used macro assemblers ;-), but the language has two special keywords: static and dynamic, where code annotated with static runs in the "compiler domain", and code annotated with dynamic runs in "application domain". Of course, I don't know much about this, so this idea might be totally insane ;-) Probably this is impossible because of the halting problem or something... Pete Don Stewart wrote: Better here means "better" -- a functional language on the type system, to type a functional language on the value level. -- Don For a taste, see Instant Insanity transliterated in this functional language: http://hpaste.org/2689 NB: it took me 5 minutes, and that was my first piece of coding ever with Type families Wow. Great work! The new age of type hackery has dawned. -- Don ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -BEGIN PGP SIGNATURE- Version: GnuPG v1.4.7 (MingW32) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org iD8DBQFG6ikc11V8mqIQMRsRA+PzAKCN0bC6lv8p9WEwJkJrcczktIdKGACfUdkt 0QBGlmgwfYrKS6lKEwQihkc= =31jo -END PGP SIGNATURE- ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Monad.Reader 8: Haskell, the new C++
-BEGIN PGP SIGNED MESSAGE- Hash: RIPEMD160 I heard only rumors, but isn't Lisp supposed to be just that? A programmable programming language? Peter Verswyvelen schrieb: > This is all very cool stuff, but sometimes I wander if it isn't possible > to drop the special languages for fiddling with types, and introduce > just a single language which has no types, only raw data from which you > can built your own "types" (as in the old days when we used macro > assemblers ;-), but the language has two special keywords: static and > dynamic, where code annotated with static runs in the "compiler domain", > and code annotated with dynamic runs in "application domain". Of course, > I don't know much about this, so this idea might be totally insane ;-) > Probably this is impossible because of the halting problem or something... > > Pete > > Don Stewart wrote: Better here means "better" -- a functional language on the type system, to type a functional language on the value level. -- Don >>> For a taste, see Instant Insanity transliterated in this functional >>> language: >>> >>> http://hpaste.org/2689 >>> >>> NB: it took me 5 minutes, and that was my first piece of coding ever >>> with Type families >>> >> >> Wow. Great work! >> The new age of type hackery has dawned. >> >> -- Don >> ___ >> Haskell-Cafe mailing list >> Haskell-Cafe@haskell.org >> http://www.haskell.org/mailman/listinfo/haskell-cafe >> >> >> > > ___ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe -BEGIN PGP SIGNATURE- Version: GnuPG v1.4.7 (MingW32) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org iD8DBQFG6ikc11V8mqIQMRsRA+PzAKCN0bC6lv8p9WEwJkJrcczktIdKGACfUdkt 0QBGlmgwfYrKS6lKEwQihkc= =31jo -END PGP SIGNATURE- ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Monad.Reader 8: Haskell, the new C++
PS: And, no, you won't be able to set breakpoints in type-level programs... but will i be able to lift type-level programs to the kind level? :-) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Monad.Reader 8: Haskell, the new C++
On 9/14/07, Thomas Schilling <[EMAIL PROTECTED]> wrote: > The type system doesn't help you avoid writing non-terminating programs, > so i see no problem with it being possible giving programmers the power > to express and check more complex properties of their programs -- as > long as type-checking remains sound. From a practical standpoint, > non-terminating type checks are just as much a bug as non-terminating > library functions. Type systems need more thought anyways, so why not > make sure it's terminating, too? The other extreme is to use dependent > types everywhere, but this has a bit more drastic consequences to the > accessibility and practicality of the language. While I love all the exceedingly cool type hackery, I also like the compiler to terminate. Some people in this forum may be old enough to remember Turbo Prolog. It did mode inference (i.e. data-flow analysis) on programs, but unfortunately it didn't always terminate. So what you got was a hung compiler, leaving you to guess what it was about your [quite possibly correct] program that caused the analysis to loop. With C++ templates, the problem is addressed by having a limit to the depth of the "call stack" for template evaluation. I recall with Forte 5, there was no flag to let you increase the depth, so at one point we had to do something like if (0) { // Horrible nasty expression to force the evaluation of some of the // the lower parts of the template stack } This works because (at least in Forte 5, and probably most implementations) template instantiations are hash-consed. I would *much* rather have a simpler type system, than a compiler which might not terminate. cheers, T. -- Thomas Conway [EMAIL PROTECTED] Silence is the perfectest herald of joy: I were but little happy, if I could say how much. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Monad.Reader 8: Haskell, the new C++
On Fri, Sep 14, 2007 at 11:05:34AM +1000, Manuel M T Chakravarty wrote: > Just to complete transferring the discussion from the ephemeral hpaste to > the mailing list. My response to the lack of being able to display > normalised types was that GHC actually goes to considerable trouble to > preserve the original (non-normalised types) for error messages and other > output, as this usually makes these messages easier to understand (eg, you > usually rather like String than [Char] in an error message). That's what they always say, but IME GHC's unpredictable mixing of expanded and unexpanded form is more confusing than a straight macro-expansion would be. What are the motivating examples (ideally I'd like a mailing list thread or paper citation)? Stefan signature.asc Description: Digital signature ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Monad.Reader 8: Haskell, the new C++
Derek Elkins wrote, On Thu, 2007-09-13 at 11:12 -0700, Don Stewart wrote: Better here means "better" -- a functional language on the type system, to type a functional language on the value level. -- Don For a taste, see Instant Insanity transliterated in this functional language: http://hpaste.org/2689 NB: it took me 5 minutes, and that was my first piece of coding ever with Type families Wow. Great work! The new age of type hackery has dawned. Is the type level functional language non-strict? (Is there a flag that will allow non-terminating associated type programs?) The associated type theory is only concerned with terminating (aka strongly normalising) sets of type instances. For a strongly normalising calculus, it does not matter whether you use eager or non-strict evaluation. However, there is of course a flag to diable the check for termination and to give up on decidable type checking.[1] It's the same flag as for type classes: -fallow-undecidable-instances (Equations of type families, or type-level functions, are introduced with the keywords "type instance", so the option name still makes sense.) FWIW, the evaluation strategy in this case is right now fairly eager, but it is a little hard to characterise. If the application of a type family needs to be normalised to proceed with unification, eg, [a] ~ F (G Int) then F (G Int) will be eagerly evaluated (ie, first G Int, and then (F ). However, type-level data constructors (ie, type constructors are non-strict); eg, [a] ~ [F Int] will result in the substitution [F Int/a]. And you can use cyclic bindings: a ~ F a However, they must have a finite solution, as we still only admit finite types; eg, the following definition of F would be fine: type family F a type instance F a = Int but type family F a type instance F a = [a] will give you one of these "cannot construct infinite type: a ~ [a]" messages. This makes it a bit like Id/pH's lenient evaluation. Manuel [1] This is GHC after all, it tries to gently nudge you in the right direction, but if you insist, it happily let's you drill arbitrarily large holes in your foot. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Monad.Reader 8: Haskell, the new C++
Pepe Iborra wrote, For a taste, see Instant Insanity transliterated in this functional language: http://hpaste.org/2689 I thought I'd better paste here the code for Instant Insanity with Type Families. Otherwise it will vanish in a short time. I took the opportunity to clean it up a bit. Thanks! Although AT are not a supported feature, the code works in a 6.8.1 snapshot. But note that you cannot actually see the solution, as there is no way to ask GHCi to display the normalized types. Just to complete transferring the discussion from the ephemeral hpaste to the mailing list. My response to the lack of being able to display normalised types was that GHC actually goes to considerable trouble to preserve the original (non-normalised types) for error messages and other output, as this usually makes these messages easier to understand (eg, you usually rather like String than [Char] in an error message). However, to debug your type-level programs (or to abuse the type checker as an evaluator) this is clearly inconvenient. So, the plan is to add a ghci command that given a type will print its normal form. On hpaste, Pepe also suggested a flag to instruct the compiler to generally print normalised instead of unnormalised types. However, I think a form of eval for types on the command line is the most direct way of experimenting with type families and debugging type-level programs. Manuel PS: And, no, you won't be able to set breakpoints in type-level programs... ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Monad.Reader 8: Haskell, the new C++
On Fri, 2007-09-14 at 10:42 +1200, ok wrote: > I wrote: > >> Since not all Turing machines halt, and since the halting problem is > >> undecidable, this means not only that some Haskell programs will make > >> the type checker loop forever, but that there is no possible meta- > >> checker that could warn us when that would happen. > > On 13 Sep 2007, at 4:27 pm, Stefan Holdermans wrote: > > Do not forget that both functional dependencies and associated > > types come with syntactic restrictions that are there just to > > "tame" the Turing completeness, i.e., to guarantee that type > > checking will actually terminate. > > I don't know anything about associated types, so can't comment on those. > But on the subject of functional dependencies, you and the author of the > article in Monad.Reader 8 *cannot* both be right, because the whole > point of that article is to explain how to program in the type system, > using, amongst other things, conditionals and recursion, in such a way > that a Turing machine can surely be simulated. If there is some > restriction to guarantee termination, then those techniques can't work. > > > > > Admittedly, it's my experience that whenever one wants to do > > something interesting (and here I mean "interesting" in a way that > > you would probably label as "rather twisted" ;-)), one has to > > bypass these restrictions (and, hence, allow for potentially > > undecidable instances). > > Ah, now we have it. To quote Conrad Parker: > This tutorial uses the Haskell98 type system extended with > multi-parameter typeclasses and undecidable instances. > We need to enable some GHC extensions to play with this type- > hackery: > $ ghci -fglasgow-exts -fallow-undecidable-instances > > That is the combination I'm talking about. > > > Now, I haven't really worked with associated types (or, for that > > matter, associated type synonyms), but my hope is that, when using > > those, turning off the checks is needed less often. We'll see. > > If you hope that, then we probably agree more than you might think. > My point is that the combination exists and is being explained so that > people can use it, and that the result is comparable in C++. (Imagine > Dame Edna Everage saying "I mean that in a loving way, possums.") The type system doesn't help you avoid writing non-terminating programs, so i see no problem with it being possible giving programmers the power to express and check more complex properties of their programs -- as long as type-checking remains sound. From a practical standpoint, non-terminating type checks are just as much a bug as non-terminating library functions. Type systems need more thought anyways, so why not make sure it's terminating, too? The other extreme is to use dependent types everywhere, but this has a bit more drastic consequences to the accessibility and practicality of the language. I don't think this will become a mainstream tool any time soon, but it may turn out to be very valuable to library authors. We also shouldn't forget that this is a brand-new feature and requires proper evaluation; how better could this be achieved than by having it included as an optional feature in a mature and well-used compiler? I am glad that Haskellers try to integrate theory and practice that nicely. / Thomas ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Monad.Reader 8: Haskell, the new C++
I wrote: Since not all Turing machines halt, and since the halting problem is undecidable, this means not only that some Haskell programs will make the type checker loop forever, but that there is no possible meta- checker that could warn us when that would happen. On 13 Sep 2007, at 4:27 pm, Stefan Holdermans wrote: Do not forget that both functional dependencies and associated types come with syntactic restrictions that are there just to "tame" the Turing completeness, i.e., to guarantee that type checking will actually terminate. I don't know anything about associated types, so can't comment on those. But on the subject of functional dependencies, you and the author of the article in Monad.Reader 8 *cannot* both be right, because the whole point of that article is to explain how to program in the type system, using, amongst other things, conditionals and recursion, in such a way that a Turing machine can surely be simulated. If there is some restriction to guarantee termination, then those techniques can't work. Admittedly, it's my experience that whenever one wants to do something interesting (and here I mean "interesting" in a way that you would probably label as "rather twisted" ;-)), one has to bypass these restrictions (and, hence, allow for potentially undecidable instances). Ah, now we have it. To quote Conrad Parker: This tutorial uses the Haskell98 type system extended with multi-parameter typeclasses and undecidable instances. We need to enable some GHC extensions to play with this type- hackery: $ ghci -fglasgow-exts -fallow-undecidable-instances That is the combination I'm talking about. Now, I haven't really worked with associated types (or, for that matter, associated type synonyms), but my hope is that, when using those, turning off the checks is needed less often. We'll see. If you hope that, then we probably agree more than you might think. My point is that the combination exists and is being explained so that people can use it, and that the result is comparable in C++. (Imagine Dame Edna Everage saying "I mean that in a loving way, possums.") ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Monad.Reader 8: Haskell, the new C++
On Thu, 2007-09-13 at 11:12 -0700, Don Stewart wrote: > > >Better here means "better" -- a functional language on the type > > >system, > > >to type a functional language on the value level. > > > > > >-- Don > > > > For a taste, see Instant Insanity transliterated in this functional > > language: > > > > http://hpaste.org/2689 > > > > NB: it took me 5 minutes, and that was my first piece of coding ever > > with Type families > > Wow. Great work! > > The new age of type hackery has dawned. Is the type level functional language non-strict? (Is there a flag that will allow non-terminating associated type programs?) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Monad.Reader 8: Haskell, the new C++
This is all very cool stuff, but sometimes I wander if it isn't possible to drop the special languages for fiddling with types, and introduce just a single language which has no types, only raw data from which you can built your own "types" (as in the old days when we used macro assemblers ;-), but the language has two special keywords: static and dynamic, where code annotated with static runs in the "compiler domain", and code annotated with dynamic runs in "application domain". Of course, I don't know much about this, so this idea might be totally insane ;-) Probably this is impossible because of the halting problem or something... Pete Don Stewart wrote: Better here means "better" -- a functional language on the type system, to type a functional language on the value level. -- Don For a taste, see Instant Insanity transliterated in this functional language: http://hpaste.org/2689 NB: it took me 5 minutes, and that was my first piece of coding ever with Type families Wow. Great work! The new age of type hackery has dawned. -- Don ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Monad.Reader 8: Haskell, the new C++
> >Better here means "better" -- a functional language on the type > >system, > >to type a functional language on the value level. > > > >-- Don > > For a taste, see Instant Insanity transliterated in this functional > language: > > http://hpaste.org/2689 > > NB: it took me 5 minutes, and that was my first piece of coding ever > with Type families Wow. Great work! The new age of type hackery has dawned. -- Don ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Monad.Reader 8: Haskell, the new C++
For a taste, see Instant Insanity transliterated in this functional language: http://hpaste.org/2689 I thought I'd better paste here the code for Instant Insanity with Type Families. Otherwise it will vanish in a short time. I took the opportunity to clean it up a bit. Although AT are not a supported feature, the code works in a 6.8.1 snapshot. But note that you cannot actually see the solution, as there is no way to ask GHCi to display the normalized types. My favorite bit is: *> type instance Map f Nil = Nil *> type instance Map f (x:::xs) = Apply f x ::: Map f xs \begin{code} import Prelude hiding (all, flip, map, filter) u = undefined data R -- Red data G -- Green data B -- Blue data W -- White data Cube u f r b l d type CubeRed = Cube R R R R R R type CubeBlue = Cube B B B B B B type Cube1 = Cube B G W G B R type Cube2 = Cube W G B W R R type Cube3 = Cube G W R B R R type Cube4 = Cube B R G G W W data True data False type family And b1 b2 type instance And True True = True type instance And True False= False type instance And False True = False type instance And False False= False data Nil data Cons x xs data x ::: xs infixr 5 ::: type family ListConcat l1 l2 type instance ListConcat Nil l = l type instance ListConcat (x:::xs) ys = x:::(ListConcat xs ys) type family Apply f a data Rotation data Twist data Flip type instance Apply Rotation (Cube u f r b l d) = Cube u r b l f d type instance Apply Twist(Cube u f r b l d) = Cube f r u l d b type instance Apply Flip (Cube u f r b l d) = Cube d l b r f u type family Map f xs type instance Map f Nil = Nil type instance Map f (x:::xs) = Apply f x ::: Map f xs type family Filter f xs type instance Filter f Nil = Nil type instance Filter f (x:::xs) = AppendIf (Apply f x) x (Filter f xs) type family AppendIf b x ys type instance AppendIf True x ys = x ::: ys type instance AppendIf False x ys = ys type family MapAppend f xs type instance MapAppend f Nil = Nil type instance MapAppend f (x:::xs) = ListConcat (x:::xs) (Map f (x:::xs)) type family MapAppend2 f xs type instance MapAppend2 f Nil = Nil type instance MapAppend2 f (x:::xs) = ListConcat (x:::xs) (MapAppend f (Map f (x:::xs))) type family MapAppend3 f xs type instance MapAppend3 f Nil = Nil type instance MapAppend3 f (x:::xs) = ListConcat xs (MapAppend2 f (Map f (x:::xs))) data Orientations type instance Apply Orientations c = MapAppend3 Rotation ( MapAppend2 Twist ( MapAppend Flip (c:::Nil))) type family NE x y type instance NE R R = False type instance NE R G = True type instance NE R B = True type instance NE R W = True type instance NE G R = True type instance NE G G = False type instance NE G B = True type instance NE G W = True type instance NE B R = True type instance NE B G = True type instance NE B B = False type instance NE B W = True type instance NE W R = True type instance NE W G = True type instance NE W B = True type instance NE W W = False type family All l type instance All Nil = True type instance All (False ::: xs) = False type instance All (True ::: xs) = All xs type family Compatible c1 c2 type instance Compatible (Cube u1 f1 r1 b1 l1 d1) (Cube u2 f2 r2 b2 l2 d2) = All (NE f1 f2 ::: NE r1 r2 ::: NE b1 b2 ::: NE l1 l2) type family Allowed c cs type instance Allowed c Nil = True type instance Allowed c (y ::: ys) = And (Compatible c y) (Allowed c ys) type family Solutions cs type instance Solutions Nil = (Nil ::: Nil) type instance Solutions (c ::: cs) = AllowedCombinations (Apply Orientations c) (Solutions cs) type family AllowedCombinations os sols type instance AllowedCombinations os Nil = Nil type instance AllowedCombinations os (s ::: sols) = ListConcat (AllowedCombinations os sols) (MatchingOrientations os s) type family MatchingOrientations os sol type instance MatchingOrientations Nil sol = Nil type instance MatchingOrientations (o ::: os) sol = AppendIf (Allowed o sol) (o:::sol) (MatchingOrientations os sol) type Cubes = (Cube1 ::: Cube2 ::: Cube3 ::: Cube4 ::: Nil) solution = u :: Solutions Cubes \end{code} ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Monad.Reader 8: Haskell, the new C++
On 13/09/2007, at 0:06, Don Stewart wrote: ok: In Monad.Reader 8, Conrad Parker shows how to solve the Instant Insanity puzzle in the "Haskell" type system. Along the way he demonstrates very clearly something that was implicit in Mark Jones' "Type Classes with Functional Dependencies" paper if you read it very very carefully (which I hadn't, but on re-reading it is there). That is, Haskell types plus multiparameter type classes plus functional dependencies is a logic programming language. In fact it is a sufficiently powerful language to emulate any Turing machine calculation as a type checking problem. So we have C++ : imperative language whose type system is a Turing-complete functional language (with rather twisted syntax) Haskell: functional language whose type system is a Turing- complete logic programming language (with rather twisted syntax) Since not all Turing machines halt, and since the halting problem is undecidable, this means not only that some Haskell programs will make the type checker loop forever, but that there is no possible meta- checker that could warn us when that would happen. I've been told that functional dependencies are old hat and there is now something better. I suspect that "better" here means "worse". Better here means "better" -- a functional language on the type system, to type a functional language on the value level. -- Don For a taste, see Instant Insanity transliterated in this functional language: http://hpaste.org/2689 NB: it took me 5 minutes, and that was my first piece of coding ever with Type families ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Monad.Reader 8: Haskell, the new C++
C++ : imperative language whose type system is a Turing-complete functional language (with rather twisted syntax) Haskell: functional language whose type system is a Turing- complete logic programming language (with rather twisted syntax) Since not all Turing machines halt, and since the halting problem is undecidable, this means not only that some Haskell programs will make the type checker loop forever, but that there is no possible meta- checker that could warn us when that would happen. Do not forget that both functional dependencies and associated types come with syntactic restrictions that are there just to "tame" the Turing completeness, i.e., to guarantee that type checking will actually terminate. (I do agree that these restrictions, for functional dependencies anyway, can be thought of as twisted in their own right, but then again, there's no such thing as a free lunch.) Admittedly, it's my experience that whenever one wants to do something interesting (and here I mean "interesting" in a way that you would probably label as "rather twisted" ;-)), one has to bypass these restrictions (and, hence, allow for potentially undecidable instances). Now, I haven't really worked with associated types (or, for that matter, associated type synonyms), but my hope is that, when using those, turning off the checks is needed less often. We'll see. Another option would be not to care that much about looping type checkers: when it loops, you'll probabely notice it quite soon already :-). That said, that would not be the option I'd pick though: being restricted to, say, structural recursion on the type-level could well cause your type-level programs to be better organised. Cheers, Stefan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Monad.Reader 8: Haskell, the new C++
ok: > In Monad.Reader 8, Conrad Parker shows how to solve the Instant Insanity > puzzle in the "Haskell" type system. Along the way he demonstrates very > clearly something that was implicit in Mark Jones' "Type Classes with > Functional Dependencies" paper if you read it very very carefully (which > I hadn't, but on re-reading it is there). That is, Haskell types plus > multiparameter type classes plus functional dependencies is a logic > programming language. In fact it is a sufficiently powerful language to > emulate any Turing machine calculation as a type checking problem. > > So we have > > C++ : imperative language whose type system is a Turing-complete > functional language (with rather twisted syntax) > > Haskell: functional language whose type system is a Turing- > complete logic programming language (with rather twisted > syntax) > > Since not all Turing machines halt, and since the halting problem is > undecidable, this means not only that some Haskell programs will make > the type checker loop forever, but that there is no possible meta- > checker that could warn us when that would happen. > > I've been told that functional dependencies are old hat and there is > now something better. I suspect that "better" here means "worse". Better here means "better" -- a functional language on the type system, to type a functional language on the value level. -- Don ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Monad.Reader 8: Haskell, the new C++
ok wrote: So we have C++ : imperative language whose type system is a Turing-complete functional language (with rather twisted syntax) Haskell: functional language whose type system is a Turing- complete logic programming language (with rather twisted syntax) They also have twisted semantics. I've been told that functional dependencies are old hat and there is now something better. I suspect that "better" here means "worse". Lattice duality, Galois connections, functor adjunctions, etc., have taught me that better is always equivalent to worse. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Monad.Reader 8: Haskell, the new C++
In Monad.Reader 8, Conrad Parker shows how to solve the Instant Insanity puzzle in the "Haskell" type system. Along the way he demonstrates very clearly something that was implicit in Mark Jones' "Type Classes with Functional Dependencies" paper if you read it very very carefully (which I hadn't, but on re-reading it is there). That is, Haskell types plus multiparameter type classes plus functional dependencies is a logic programming language. In fact it is a sufficiently powerful language to emulate any Turing machine calculation as a type checking problem. So we have C++ : imperative language whose type system is a Turing-complete functional language (with rather twisted syntax) Haskell: functional language whose type system is a Turing- complete logic programming language (with rather twisted syntax) Since not all Turing machines halt, and since the halting problem is undecidable, this means not only that some Haskell programs will make the type checker loop forever, but that there is no possible meta- checker that could warn us when that would happen. I've been told that functional dependencies are old hat and there is now something better. I suspect that "better" here means "worse". ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe