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++
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++
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++
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++
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++
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++
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++
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 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++
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++
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 result of G Int). 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++
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++
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++
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
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++
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
