Yes, Bluespec has efficient type level naturals. But it only has
arithmetic and some trivial decision procedures. The slogan is "the
type checker knows arithmetic, not algebra".
It worked pretty well. But you soon get into situations where you
need polymorphic recursion of functions with type level naturals. It
needs careful consideration (I never implemented that for Bluespec).
-- Lennart
On Dec 22, 2006, at 14:28 , Jan-Willem Maessen wrote:
On Dec 21, 2006, at 5:03 PM, Jacques Carette wrote:
...
What must be remembered is that full dependent types are NOT
needed to get a lot of the benefits of dependent-like types. This
is what some of Oleg's type gymnastics shows (and others too). My
interest right now lies in figuring out exactly how much can be
done statically.
For example, if one had decent naturals at the type level (ie
naturals encoded not-in-unary) with efficient arithmetic AND a few
standard decision procedures (for linear equalities and
inequalities say), then most of the things that people currently
claim need dependent types are either decidable or have very
strong heuristics that "work" [1].
My understanding is that BlueSpec did roughly this. As we're
discovering in Fortress, type-level naturals are a big help; faking
it really is horrible, as unary representations are unusable for
real work and digital representations require a ton of stunts to
get the constraints to solve in every direction (and they're still
ugly).
I for one would welcome a simple extension of Haskell with type-
level nats (the implementor gets to decide if they're a new kind,
or can interact with * somehow).
-Jan-Willem Maessen
[PS: hadn't seen the LNCS reference before, thanks to Jacques for
sending that along.]
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
