#4385: Type-level natural numbers
----------------------------------------+-----------------------------------
Reporter: diatchki | Owner: diatchki
Type: feature request | Status: new
Priority: normal | Milestone: 7.2.1
Component: Compiler (Type checker) | Version:
Keywords: | Testcase:
Blockedby: | Difficulty:
Os: Unknown/Multiple | Blocking:
Architecture: Unknown/Multiple | Failure: None/Unknown
----------------------------------------+-----------------------------------
Comment(by diatchki):
Hello,
I added some support for associativity over the weekend, and now the (+++)
example works (I've pushed the changes to the git repo).
On the pattern matching issue: I also thought that using the unary
representation might be clunky, but I played around with it this weekend,
and I kind of like it. It leads to fairly natural looking definitions of
simple inductive functions, and I don't think that it is even that
inefficient---the unary number is lazily generated so it essentially
corresponds to a sequence of checks on the real integer. Here is the code
I played around with:
http://hackage.haskell.org/trac/ghc/wiki/TypeNats/InductiveDefinitions
We might even be able to add a "fold" to deforest the intermediate "Zero"
and "Succ" constructors.
(Previously, I was thinking that we should use type classes to do this
sort of thing, but GHC does not like type functions in instance heads, and
also we'd had to let it know that (x + 1) does not overlap with 0, etc.,
so overall this seems more complex.)
Finally a general note :-) I also think that this sort of "fake dependent
types" / GADT programs are neat and useful but I wouldn't want to raise
expectations too much because we really are pushing at the edges of
Haskell's type system here---these simple examples use a lot of machinery
(qualified types, type functions, GADTs, polymorphic recursion).
Another useful technique is to use type-level naturals as "phantom" types
to provide safe library wrappers to unsafe primitives. This is a sort of
intermediate step between the current state of Haskell and the dependent
type/GADT world because it provides safety to the users of the library but
only as long as the library is written correctly (i.e., the types do not
help the library writer, but they help the library user). Here is an
example of the technique:
{{{
newtype Vec (n :: Nat) a = Vec [a]
empty :: Vec 0 a
empty = Vec []
mapVec :: (a -> b) -> Vec n a -> Vec n b
mapVec f (Vec xs) = Vec (map f xs)
catVec :: Vec m a -> Vec n a -> Vec (m + n) a
catVec (Vec xs) (Vec ys) = Vec (xs ++ ys)
-- etc..
}}}
Note that here the types express the library writer's intention, but they
do not enforce the correctness of the implementation. The benefit is that
there are no complicated constraints to solve. Of course, constraints
will arise when we use the library, but as long as the use is at concrete
types, then the constraints would be easy to solve.
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/4385#comment:21>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
