Re: [Haskell-cafe] Re: Type-level arithmetic
On Fri, 2007-10-12 at 13:52 -0400, Steve Schafer wrote: On Fri, 12 Oct 2007 18:24:38 +0100, you wrote: I was actually thinking more along the lines of a programming language where you can just write head :: (n 1) = List n x - x tail :: List n x - List (n-1) x (++) :: List n x - List m x - List (n+m) x and so forth. How, then, is that any different from a general-purpose programming language? You're just drawing the line in the sand in a different place. You end up with a programming system where compilation is a side effect of executing the real program. I'd use that language... jcc ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Type-level arithmetic
Manuel M T Chakravarty writes: Ross Paterson wrote, On Tue, Oct 16, 2007 at 10:56:27AM +1000, Manuel M T Chakravarty wrote: Lennart Augustsson wrote, And Haskell embedded a logical programming language on accident. Well, we are just trying to fix that :) Since types are inferred using unification, and classes are still present, adding functions yields a functional logic programming language at the type level. I used to agree with that, but I changed my opinion. Or more precisely, I'd say that it is a very weak functional logic language. Weak in the sense that it's logic component is essential nil. Let me justify this statement. We have type variables that are like logical variables in logic programming languages. However, we never use function definitions to guess values for type variables. Instead, function evaluation simplify suspends when it depends on an uninstantiated variable and resumes when this variable becomes instantiated. (The functional logic people call this evaluation strategy residuation.) For example, if we have type family T a type instance T Int = Char then, given (T a ~ Char), we do *not* execute T backwards and infer (a = Int). Instead, we leave (T a ~ Char) as it is and evaluate 'T' only when 'a' becomes fixed. Explained slightly differently. The above type function is open (hence, we only apply matching) whereas in functional logic programming type functions are closed (therefore, we use unification/residuation). Such an approach fits well together with open type classes as found in Haskell. Martin There have been proposals for truely functional logic languages using residuation, but they include support for backtracking and producing multiple solutions to a single query. We support neither on the type level. So, the only interaction between type functions and unification left is that function evaluation suspends on uninstantiated type variables and resumes when they become instantiated. This is not functional logic programming, it is *concurrent* functional programming with single-assignment variables. In fact, languages such as Id and pH, which are routinely characterised as concurrent functional, use exactly this model. I don't think the presence of type classes *without* functional dependencies changes this. Manuel PS: You get a *real* functional logic language by truly performing unification modulo an equational theory. This leads to the concept of E-unification and, in our constructor-based context, to narrowing as an evaluation strategy. ___ 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] Re: Type-level arithmetic
Ross Paterson wrote, On Tue, Oct 16, 2007 at 10:56:27AM +1000, Manuel M T Chakravarty wrote: Lennart Augustsson wrote, And Haskell embedded a logical programming language on accident. Well, we are just trying to fix that :) Since types are inferred using unification, and classes are still present, adding functions yields a functional logic programming language at the type level. I used to agree with that, but I changed my opinion. Or more precisely, I'd say that it is a very weak functional logic language. Weak in the sense that it's logic component is essential nil. Let me justify this statement. We have type variables that are like logical variables in logic programming languages. However, we never use function definitions to guess values for type variables. Instead, function evaluation simplify suspends when it depends on an uninstantiated variable and resumes when this variable becomes instantiated. (The functional logic people call this evaluation strategy residuation.) For example, if we have type family T a type instance T Int = Char then, given (T a ~ Char), we do *not* execute T backwards and infer (a = Int). Instead, we leave (T a ~ Char) as it is and evaluate 'T' only when 'a' becomes fixed. There have been proposals for truely functional logic languages using residuation, but they include support for backtracking and producing multiple solutions to a single query. We support neither on the type level. So, the only interaction between type functions and unification left is that function evaluation suspends on uninstantiated type variables and resumes when they become instantiated. This is not functional logic programming, it is *concurrent* functional programming with single-assignment variables. In fact, languages such as Id and pH, which are routinely characterised as concurrent functional, use exactly this model. I don't think the presence of type classes *without* functional dependencies changes this. Manuel PS: You get a *real* functional logic language by truly performing unification modulo an equational theory. This leads to the concept of E-unification and, in our constructor-based context, to narrowing as an evaluation strategy. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Type-level arithmetic
On Tue, Oct 16, 2007 at 10:56:27AM +1000, Manuel M T Chakravarty wrote: Lennart Augustsson wrote, And Haskell embedded a logical programming language on accident. Well, we are just trying to fix that :) Since types are inferred using unification, and classes are still present, adding functions yields a functional logic programming language at the type level. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Type-level arithmetic
And Haskell embedded a logical programming language on accident. On 10/15/07, Manuel M T Chakravarty [EMAIL PROTECTED] wrote: Dan Piponi wrote, On 10/12/07, Brandon S. Allbery KF8NH [EMAIL PROTECTED] wrote: He wants to write entire programs in the type system, something like the crazies who write programs in C++ templates such that template expansion does all the work at compile time Crazies? :-) http://homepage.mac.com/sigfpe/Computing/peano.html Having switched from C++ to Haskell (at least in my spare time) I thought I'd escaped that kind of type hackery but it seems to be following me... The way I see, we are trying to come up with a clean way of providing type-level computations (ie, we use and extend the standard theory of HM type systems). C++ embedded a functional language in the type systems mostly by accident, whereas we do it on purpose. Manuel ___ 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] Re: Type-level arithmetic
Lennart Augustsson wrote, And Haskell embedded a logical programming language on accident. Well, we are just trying to fix that :) On 10/15/07, *Manuel M T Chakravarty* [EMAIL PROTECTED] mailto:[EMAIL PROTECTED] wrote: Dan Piponi wrote, On 10/12/07, Brandon S. Allbery KF8NH [EMAIL PROTECTED] mailto:[EMAIL PROTECTED] wrote: He wants to write entire programs in the type system, something like the crazies who write programs in C++ templates such that template expansion does all the work at compile time Crazies? :-) http://homepage.mac.com/sigfpe/Computing/peano.html Having switched from C++ to Haskell (at least in my spare time) I thought I'd escaped that kind of type hackery but it seems to be following me... The way I see, we are trying to come up with a clean way of providing type-level computations (ie, we use and extend the standard theory of HM type systems). C++ embedded a functional language in the type systems mostly by accident, whereas we do it on purpose. Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Type-level arithmetic
Dan Piponi wrote, On 10/12/07, Brandon S. Allbery KF8NH [EMAIL PROTECTED] wrote: He wants to write entire programs in the type system, something like the crazies who write programs in C++ templates such that template expansion does all the work at compile time Crazies? :-) http://homepage.mac.com/sigfpe/Computing/peano.html Having switched from C++ to Haskell (at least in my spare time) I thought I'd escaped that kind of type hackery but it seems to be following me... The way I see, we are trying to come up with a clean way of providing type-level computations (ie, we use and extend the standard theory of HM type systems). C++ embedded a functional language in the type systems mostly by accident, whereas we do it on purpose. Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Type-level arithmetic
Andrew Coppin wrote:
I was actually thinking more along the lines of a programming language
where you can just write
head :: (n 1) = List n x - x
Current GHC can approximate this with a GADT:
==
{-# OPTIONS -fglasgow-exts #-}
module SafeHead where
data Z
data S a
data List n a where
Nil :: List Z a
Cons :: a - List n a - List (S n) a
head1 :: List (S n) a - a
head1 (Cons x _) = x
-- head1 Nil = undefined -- error: inaccessible
-- test0 = head1 Nil -- error: Z /= S n
test1 = head1 (Cons 'a' Nil)
==
For more complex type arithmetic, you need the GHC 6.8RC for type families:
==
data TT -- true
data FF -- false
type family Geq a b -- a = b
type instance Geq a Z = TT
type instance Geq Z (S n) = FF
type instance Geq (S n) (S m) = Geq n m
head2 :: Geq n (S Z) ~ TT = List n a - a
head2 (Cons x _) = x
-- head2 Nil = undefined -- no error, but useless
-- test2 = head2 Nil -- error: TT /= Geq Z (S Z)
test3 = head2 (Cons 'a' Nil)
==
Of course, the downside is that using the List GADT can be inconvenient
since you need to be able to express _in a static way_ the length of the
lists:
(++) :: List n a - List m a - List (Sum n m) a
(\\) :: List n a - List m a - List (???) a
The (\\) case is impossible to predict (if you know only the lengths),
so you probably need to return a simple [a] there. Of course, you can
recover a better type with un-time checks, as in (roughly)
checkLength :: [a] - n - Maybe (List n a)
Regards,
Zun.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Type-level arithmetic
On Fri, 12 Oct 2007 18:24:38 +0100, you wrote: I was actually thinking more along the lines of a programming language where you can just write head :: (n 1) = List n x - x tail :: List n x - List (n-1) x (++) :: List n x - List m x - List (n+m) x and so forth. How, then, is that any different from a general-purpose programming language? You're just drawing the line in the sand in a different place. You end up with a programming system where compilation is a side effect of executing the real program. Steve Schafer Fenestra Technologies Corp. http://www.fenestra.com/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Type-level arithmetic
On 10/12/07, Andrew Coppin [EMAIL PROTECTED] wrote: I was actually thinking more along the lines of a programming language where you can just write head :: (n 1) = List n x - x tail :: List n x - List (n-1) x (++) :: List n x - List m x - List (n+m) x and so forth. You know, instead of the elaborate simulations crafted out of systems that weren't meant to do this stuff. You might be interested in Epigram: http://e-pig.org/ The paper at: http://www.e-pig.org/downloads/epigram-notes.pdf has an example like your head/tail example (in section 3, Vectors and finite sets). Cheers, Tim -- Tim Chevalier * catamorphism.org * Often in error, never in doubt I always feel I have to take a stand and there's always someone on hand to hate me for standing there / I always feel i have to open my mouth and every time I do I offend someone somewhere -- Ani DiFranco ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Type-level arithmetic
I was actually thinking more along the lines of a programming language where you can just write head :: (n 1) = List n x - x tail :: List n x - List (n-1) x (++) :: List n x - List m x - List (n+m) x and so forth. You know, instead of the elaborate simulations crafted out of systems that weren't meant to do this stuff. Of course, the integer case is probably fairly easy. I suspect the issue is that as soon as you try to do this kind of thing, you develop a terminal case of wanting to hyper-generalise everything which then directly results in an incomprehensible mess... ;-) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Type-level arithmetic
On 10/12/07, Steve Schafer [EMAIL PROTECTED] wrote: On Fri, 12 Oct 2007 18:24:38 +0100, you wrote: I was actually thinking more along the lines of a programming language where you can just write head :: (n 1) = List n x - x tail :: List n x - List (n-1) x (++) :: List n x - List m x - List (n+m) x and so forth. How, then, is that any different from a general-purpose programming language? It's different because the property that (for example) head requires a nonempty list is checked at compile time instead of run time. You're just drawing the line in the sand in a different place. You end up with a programming system where compilation is a side effect of executing the real program. I'm not sure exactly what you mean by that, but a lot of people are spending time thinking about ways for programmers to express more of their knowledge about programs in a way that's accessible to and checkable by compilers and other automated tools, and while you might see it as just drawing the line in the sand in a different place, you could say the same thing about programming in a language with a Haskell-like type system instead of a Lisp-like type system. Cheers, Tim -- Tim Chevalier * catamorphism.org * Often in error, never in doubt Yeah. Okay. Yeah. Basically, swingers meet ISO 9000. -- DF, on cuddle parties ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Type-level arithmetic
On 10/12/07, Steve Schafer [EMAIL PROTECTED] wrote: On Fri, 12 Oct 2007 13:03:16 -0700, you wrote: It's different because the property that (for example) head requires a nonempty list is checked at compile time instead of run time. No, I understand that. Andrew was talking about using type programming to do the things that a sane person would use ordinary programming to do. I'm not sure what sanity has to do with it. Presumably we all agree that it's a good idea for the compiler to know, at compile-time, that head is only applied to lists. Why not also have the compiler check that head is only applied to non-empty lists? If you think it's sane to want one property checked at compile-time and insane to want the other property checked at compile-time, can you describe your test that can be applied to program properties to determine whether or not it's sane to want them statically checked? And he wanted to know if there were any efforts to create a type system syntax that better supported that. But it seems to me that when you do that, the language of the type system begins to look like a general-purpose programming language. And that just shoves everything up to the next meta level. Pretty soon, you're going to need a meta-type system to meta-type-check your type language, and so on. This criticism has been made before. I'm all for enhancing the expressibility of concepts _related to typing_ within the type system, but I don't think that was the original point of this discussion. After all, Andrew's original message mentioned stuff the type system was never designed to do. What do you mean by related to typing? Haskell's type system allows us to say that head is a function that maps a list of things of type a onto a thing of type a. A more expressive type system might allow us to say that head's domain consists of *non-empty* lists. In this type system, emptiness or non-emptiness is a concept related to typing, because it's a concept that that type system can express. You seem to be criticizing richer type systems on the sole basis that they are richer than existing ones. Cheers, Tim -- Tim Chevalier * catamorphism.org * Often in error, never in doubt I always wanted to be commander-in-chief of my own one-woman army -- Ani DiFranco ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Type-level arithmetic
On Fri, 12 Oct 2007 13:03:16 -0700, you wrote: It's different because the property that (for example) head requires a nonempty list is checked at compile time instead of run time. No, I understand that. Andrew was talking about using type programming to do the things that a sane person would use ordinary programming to do. And he wanted to know if there were any efforts to create a type system syntax that better supported that. But it seems to me that when you do that, the language of the type system begins to look like a general-purpose programming language. And that just shoves everything up to the next meta level. Pretty soon, you're going to need a meta-type system to meta-type-check your type language, and so on. I'm all for enhancing the expressibility of concepts _related to typing_ within the type system, but I don't think that was the original point of this discussion. After all, Andrew's original message mentioned stuff the type system was never designed to do. Steve Schafer Fenestra Technologies Corp. http://www.fenestra.com/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Type-level arithmetic
On Fri, 12 Oct 2007 13:25:28 -0700, you wrote: I'm not sure what sanity has to do with it. Presumably we all agree that it's a good idea for the compiler to know, at compile-time, that head is only applied to lists. Why not also have the compiler check that head is only applied to non-empty lists? Again, that sort of practical application of type systems is not (as far as I know) what this discussion is about. This discussion was spawned by talk of using the type system to do truly bizarre things, such as solve the Instant Insanity puzzle. A while back, Dan Piponi posed the question of using the type system to solve one of the liar/truthteller logic problems. And so on. Steve Schafer Fenestra Technologies Corp. http://www.fenestra.com/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Type-level arithmetic
On Fri, 12 Oct 2007, Steve Schafer wrote: On Fri, 12 Oct 2007 13:25:28 -0700, you wrote: I'm not sure what sanity has to do with it. Presumably we all agree that it's a good idea for the compiler to know, at compile-time, that head is only applied to lists. Why not also have the compiler check that head is only applied to non-empty lists? Again, that sort of practical application of type systems is not (as far as I know) what this discussion is about. This discussion was spawned by talk of using the type system to do truly bizarre things, such as solve the Instant Insanity puzzle. A while back, Dan Piponi posed the question of using the type system to solve one of the liar/truthteller logic problems. And so on. Which is nevertheless the kind of power you need in order to also be able to prove precise properties. How are you going to prove that an entire class of problems is solveable (and the safety or termination of a piece of code may depend on this) if you can't prove that an individual one is? -- [EMAIL PROTECTED] A problem that's all in your head is still a problem. Brain damage is but one form of mind damage. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Type-level arithmetic
Steve said: How, then, is that any different from a general-purpose programming language? You're just drawing the line in the sand in a different place. In a way it is like drawing a line in sand. But that's a useful thing to do for a bunch of reasons. (1) When developing code, you'd like to test as much of the code as possible for reliability. But you don't necessarily know what data your code is going to run on in the future. It'd be cool if you could somehow run as much of your code as possible even without yet having the data. By having a declaration like (++) :: List n x - List m x - List (n+m) x it's almost as if the compiler gets to run a 'reduced' version of your application. You don't actually know what the elements of the list are (or even their types), and yet you can still test to see if your code handles the lists of the lengths correctly. (2) Sometimes you want to solve a problem incrementally. It's often helpful to reason first to the type we want, and then the implementation, rather than just to the implementation - it gives a way to factor the problem into two stages. By allowing some computation to take place at compile time you can be flexible about where the boundaries between your stages lie allowing you much more freedom in how you incrementally arrive at your solution. (3) In theory you can get very efficient code out of a type system where the compiler knows, for example, how long the lists are in advance. I guess you could say it's a form of partial evaluation. -- Dan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Type-level arithmetic
On Fri, 12 Oct 2007 21:51:46 +0100 (GMT Daylight Time), you wrote: Which is nevertheless the kind of power you need in order to also be able to prove precise properties. We're not talking about POWER, we're talking about SYNTAX. That the Instant Insanity problem _was_ solved using Haskell's type system is obviously proof that the power to solve that kind of problem, at least, is already there. However, the solution is convoluted and less than clear at first glance. The question is whether or not there is a way to allow such solutions to be expressed in a more natural way. To which my rejoinder is, To what end? To extend the _syntax_ of the type system in a way that allows such natural expression turns it into yet another programming language. So what have we gained? Steve Schafer Fenestra Technologies Corp. http://www.fenestra.com/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Type-level arithmetic
On Fri, 12 Oct 2007, Steve Schafer wrote: On Fri, 12 Oct 2007 21:51:46 +0100 (GMT Daylight Time), you wrote: Which is nevertheless the kind of power you need in order to also be able to prove precise properties. We're not talking about POWER, we're talking about SYNTAX. Which has no small amount to do with the power to express problems in a natural way, no? My point being that we already want this for things that are more obviously appropriate uses of a type system. To which my rejoinder is, To what end? To extend the _syntax_ of the type system in a way that allows such natural expression turns it into yet another programming language. So what have we gained? It's already yet another programming language, whether you like it or not - the question is how usable it is. Either you accept the gains made on the way or not, but what we have gained is the ability to reason about our programs in the language they are written in. We already have types-of-types in Haskell, they're called kinds. There's even a language that'll let you stack this as far as you like - why not? Zero, one or infinity, what else is new? -- [EMAIL PROTECTED] Society does not owe people jobs. Society owes it to itself to find people jobs. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Type-level arithmetic
On Oct 12, 2007, at 16:25 , Tim Chevalier wrote: On 10/12/07, Steve Schafer [EMAIL PROTECTED] wrote: On Fri, 12 Oct 2007 13:03:16 -0700, you wrote: It's different because the property that (for example) head requires a nonempty list is checked at compile time instead of run time. No, I understand that. Andrew was talking about using type programming to do the things that a sane person would use ordinary programming to do. I'm not sure what sanity has to do with it. Presumably we all agree that it's a good idea for the compiler to know, at compile-time, that head is only applied to lists. You two are talking past each other. You're talking about dependent typing, etc. Steve's complaint is not about dependent typing; he's saying Andrew is looking for something different from that, namely the type system being a metalanguage. I have the same impression, that Andrew isn't interested in dependent typing. -- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] [EMAIL PROTECTED] system administrator [openafs,heimdal,too many hats] [EMAIL PROTECTED] electrical and computer engineering, carnegie mellon universityKF8NH ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Type-level arithmetic
On 10/12/07, Brandon S. Allbery KF8NH [EMAIL PROTECTED] wrote: You two are talking past each other. You're talking about dependent typing, etc. Steve's complaint is not about dependent typing; he's saying Andrew is looking for something different from that, namely the type system being a metalanguage. Well, the type system *is* a metalanguage, so presumably Andrew's looking for something more specific than that... I have the same impression, that Andrew isn't interested in dependent typing. I'm not sure what he was really asking in his OP either, but when he said that he was looking for a language where you can write type signatures that encode list length, that certainly points to dependent types as one instance of that, even if there are other possibilities. Cheers, Tim -- Tim Chevalier * catamorphism.org * Often in error, never in doubt The way NT mounts filesystems is something I'd expect to find in a barnyard or on a stock-breeding farm.--Mike Andrews ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Type-level arithmetic
On Oct 12, 2007, at 19:26 , Tim Chevalier wrote: On 10/12/07, Brandon S. Allbery KF8NH [EMAIL PROTECTED] wrote: You two are talking past each other. You're talking about dependent typing, etc. Steve's complaint is not about dependent typing; he's saying Andrew is looking for something different from that, namely the type system being a metalanguage. Well, the type system *is* a metalanguage, so presumably Andrew's looking for something more specific than that... My impression is he's looking for something more *general* than that. He wants to write entire programs in the type system, something like the crazies who write programs in C++ templates such that template expansion does all the work at compile time and the runtime code just prints the constant result. Certainly this covers dependent typing, but it goes well beyond it. -- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] [EMAIL PROTECTED] system administrator [openafs,heimdal,too many hats] [EMAIL PROTECTED] electrical and computer engineering, carnegie mellon universityKF8NH ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Type-level arithmetic
On 10/12/07, Brandon S. Allbery KF8NH [EMAIL PROTECTED] wrote: He wants to write entire programs in the type system, something like the crazies who write programs in C++ templates such that template expansion does all the work at compile time Crazies? :-) http://homepage.mac.com/sigfpe/Computing/peano.html Having switched from C++ to Haskell (at least in my spare time) I thought I'd escaped that kind of type hackery but it seems to be following me... -- Dan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Type-level arithmetic
On Oct 12, 2007, at 19:42 , Dan Piponi wrote: On 10/12/07, Brandon S. Allbery KF8NH [EMAIL PROTECTED] wrote: He wants to write entire programs in the type system, something like the crazies who write programs in C++ templates such that template expansion does all the work at compile time Crazies? :-) http://homepage.mac.com/sigfpe/Computing/peano.html I'm not sure it's entirely sane even in Haskell, but in C++ templates it is definitely *not* sane. :) -- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] [EMAIL PROTECTED] system administrator [openafs,heimdal,too many hats] [EMAIL PROTECTED] electrical and computer engineering, carnegie mellon universityKF8NH ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
