Type-level arithmetic

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
30 messages Options
12
Reply | Threaded
Open this post in threaded view
|

Type-level arithmetic

Andrew Coppin
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
Reply | Threaded
Open this post in threaded view
|

Re: Type-level arithmetic

Dan Piponi-2
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
Reply | Threaded
Open this post in threaded view
|

Re: Type-level arithmetic

Andrew Coppin
Dan Piponi wrote:
> 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?
>  

Birthday paradox?

>> 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.
>  

Ouch. You're making my head hurt...

>> 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...
>  

...I have no idea what you just said.

(The wiki article is pretty special though. An entire raft of dense
equations with no attempt to provide any background or describe what any
of this gibberish *is*. Clearly it made sense to the author, but...)

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Type-level arithmetic

Lennart Augustsson
Yes, that web page is a terrible introduction to dependent types. :)

On 10/6/07, Andrew Coppin <[hidden email]> wrote:
Dan Piponi wrote:
> 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?
>

Birthday paradox?

>> 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.
>

Ouch. You're making my head hurt...

>> 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...
>

...I have no idea what you just said.

(The wiki article is pretty special though. An entire raft of dense
equations with no attempt to provide any background or describe what any
of this gibberish *is*. Clearly it made sense to the author, but...)

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Type-level arithmetic

David Menendez-2
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.

<http://web.cecs.pdx.edu/~sheard/>


--
Dave Menendez <[hidden email]>
<http://www.eyrie.org/~zednenem/>

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Type-level arithmetic

Manuel M T Chakravarty
In reply to this post by Andrew Coppin
Andrew Coppin wrote,
> 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!)

Type families are a step in that direction:

   http://haskell.org/haskellwiki/GHC/Type_families

Appended is a small example of defining singleton numeral types.

Manuel

-=-

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}

module Numerals
where

data Z          -- empty data type
data S a        -- empty data type

data SNat n where  -- natural numbers as singleton type
   Zero :: SNat Z
   Succ :: SNat n -> SNat (S n)

zero  = Zero
one   = Succ zero
two   = Succ one
three = Succ two
-- etc...we really would like some nicer syntax here

type family (:+:) n m :: *
type instance Z     :+: m = m
type instance (S n) :+: m = S (n :+: m)

add :: SNat n -> SNat m -> SNat (n :+: m)
add Zero     m = m
add (Succ n) m = Succ (add n m)


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Type-level arithmetic

Andrew Coppin
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
Reply | Threaded
Open this post in threaded view
|

Re: Re: Type-level arithmetic

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

Re: Re: Type-level arithmetic

Steve Schafer
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
Reply | Threaded
Open this post in threaded view
|

Re: Re: Type-level arithmetic

Bugzilla from jonathanccast@fastmail.fm
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
Reply | Threaded
Open this post in threaded view
|

Re: Re: Type-level arithmetic

Tim Chevalier
In reply to this post by Steve Schafer
On 10/12/07, Steve Schafer <[hidden email]> 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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: Type-level arithmetic

Steve Schafer
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
Reply | Threaded
Open this post in threaded view
|

Re: Re: Type-level arithmetic

Tim Chevalier
On 10/12/07, Steve Schafer <[hidden email]> 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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: Type-level arithmetic

Steve Schafer
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
Reply | Threaded
Open this post in threaded view
|

Re: Re: Type-level arithmetic

Philippa Cowderoy
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
Reply | Threaded
Open this post in threaded view
|

Re: Re: Type-level arithmetic

Steve Schafer
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
Reply | Threaded
Open this post in threaded view
|

Re: Re: Type-level arithmetic

Dan Piponi-2
In reply to this post by Steve Schafer
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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: Type-level arithmetic

Philippa Cowderoy
In reply to this post by Steve Schafer
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?

--
[hidden email]

Society does not owe people jobs.
Society owes it to itself to find people jobs.
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: Type-level arithmetic

Brandon S Allbery KF8NH
In reply to this post by Tim Chevalier

On Oct 12, 2007, at 16:25 , Tim Chevalier wrote:

> On 10/12/07, Steve Schafer <[hidden email]> 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] [hidden email]
system administrator [openafs,heimdal,too many hats] [hidden email]
electrical and computer engineering, carnegie mellon university    KF8NH


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: Type-level arithmetic

Tim Chevalier
On 10/12/07, Brandon S. Allbery KF8NH <[hidden email]> 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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
12