[Haskell-cafe] Type-level arithmetic

[Lennart Augustsson]

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

On 10/6/07, Andrew Coppin <andrewcoppin at btinternet.com> wrote:
>
> Dan Piponi wrote:
> > On 10/6/07, Andrew Coppin <andrewcoppin at btinternet.com> 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
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20071006/7c1778ec/attachment.htm