[Haskell-cafe] question on types
frodo at theshire.org
Wed Feb 18 03:20:43 EST 2009
2009/2/18 Luke Palmer <lrpalmer at gmail.com>:
> Using dependent types, you could have Prime come with a proof that the
> integer it contains is prime, and thus make those assumptions explicit and
> usable in the implementation. Unfortunately, it would be a major pain in
> the ass to do that in Haskell (for one, your algorithm would have to be
> implemented at the type level with annoying typeclasses to reify number
> types to real integers, and... yeah, people say Haskell has dependent types,
> but not in any reasonable way :-). Dependent languages like Agda, Coq, and
> Epigram are designed for this kind of thing.
I'm curious to know whether a type system exists in which such a
constraint on the type of an argument can be expressed and enforced.
In such a case, does the compiler will ever terminate the
More information about the Haskell-Cafe