[Haskell-cafe] Type-level arithmetic
lennart at augustsson.net
Sat Oct 6 17:31:53 EDT 2007
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
> >> 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
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe