deriving over renamed types
09 Apr 2002 01:05:45 +0200
Ashley Yakeley <firstname.lastname@example.org> writes:
> -- which of these types are the same?
> f1 = MkFoo undefined :: Foo Succ;
> f2 = MkFoo undefined :: Foo Succ';
> f3 = MkFoo undefined :: Foo Succ'';
> f4 = MkFoo undefined :: Foo (Add (Succ Zero));
yeah, why not! Have them all be the same thing.
(i added the missing "Foo" on f4)
add Zero b = b
add (Succ a) b = Succ (add a b)
mult Zero b = Zero
mult (Succ a) b = add b (mult a b)
fact Zero = Zero
fact (Succ n) = mult (Succ n) (fact n)
data Foo f = MkFoo (f ())
succ' = Succ
succ'' n = Succ n
-- which of these types are the same?
f1 = MkFoo undefined :: Foo Succ
f2 = MkFoo undefined :: Foo succ'
f3 = MkFoo undefined :: Foo succ''
f4 = MkFoo undefined :: Foo (add (Succ Zero))
add to haskell
- eta-expanding of (add (Succ Zero)) in (\x -> add (Succ Zero) x)
- compile-time evaluation of type expressions (handling unbounded parameters
like "x" above)
and that should do it!
I don't think this is a crazy as it sounds. Cayenne has already started
computing types at compile-time.
I'm currently working on merd (http://merd.net) which has a such a type system.
range(n, m) =
if n < m then
n | range(n + 1, m)
Two_to_height = range(2, 8) #=> 2|3|4|5|6|7|8
restricted_identity !! Two_to_height -> Two_to_height
restricted_identity(x) = x
restricted_identity(4) #=> 4
restricted_identity(1) #=> compile-time error: 1 is not in 2|3|4|5|6|7|8