deriving over renamed types

[Pixel]

Ashley Yakeley <ashley@semantic.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.
eg:

range(n, m) =
    if n < m then
        n | range(n + 1, m)
    else
        n

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