# Type-level arithmetic

30 messages
12
Open this post in threaded view
|

## Type-level arithmetic

 I've seen quite a few people do crazy things to abuse the Haskell type system in order to perform arithmetic in types. Stuff the type system was never ever intended to do. Well I was just wondering... did anybody ever sit down and come up with a type system that *is* designed for this kind of thing? What would that look like? (I'm guessing rather complex!) _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

## Re: Type-level arithmetic

 On 10/6/07, Andrew Coppin <[hidden email]> wrote: > I've seen quite a few people do crazy things to abuse the Haskell type > system in order to perform arithmetic in types. How did you know precisely what I was doing at this moment in time? > Stuff the type system > was never ever intended to do. There's "didn't intended that it be possible to" and there's "intend that it be impossible to". Hmmm...maybe one of these should be called cointend. > Well I was just wondering... did anybody ever sit down and come up with > a type system that *is* designed for this kind of thing? What would that > look like? (I'm guessing rather complex!) Well there are always languages with dependent type systems which allow you to have the type depend on a value. In such a language it's easier to make types that correspond to some mathematical constructions, like a separate type for each n-dimensional vector. (See http://www.haskell.org/haskellwiki/Dependent_type.) But that's kind of cheating. I'm guessing you're talking about a language that makes it easier to "fake" your own dependent types without properly implementing dependent types. If you find one, I could use it right now - the details of embedding the gaussian integers in Haskell types are getting a bit complicated right now... -- Dan _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

## Re: Type-level arithmetic

Open this post in threaded view
|

## Re: Type-level arithmetic

Open this post in threaded view
|

## Re: Type-level arithmetic

 In reply to this post by Dan Piponi-2 On 10/6/07, Dan Piponi <[hidden email]> wrote: > I'm guessing you're talking about a language that > makes it easier to "fake" your own dependent types without properly > implementing dependent types. If you find one, I could use it right > now - the details of embedding the gaussian integers in Haskell types > are getting a bit complicated right now... I think Î©mega was designed along those lines. -- Dave Menendez <[hidden email]> _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

## Re: Type-level arithmetic

Open this post in threaded view
|

## Re: Type-level arithmetic

 In reply to this post by Andrew Coppin 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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

## Re: Re: Type-level arithmetic

 On 10/12/07, Andrew Coppin <[hidden email]> 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.pdfhas 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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

## Re: Re: Type-level arithmetic

 In reply to this post by Andrew Coppin 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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

## Re: 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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

## Re: Re: Type-level arithmetic

Open this post in threaded view
|

## Re: 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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

## Re: Re: Type-level arithmetic

Open this post in threaded view
|

## Re: 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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

## Re: 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? -- [hidden email] 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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

## Re: 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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

## Re: Re: Type-level arithmetic

Open this post in threaded view
|

## Re: Re: Type-level arithmetic

Open this post in threaded view
|