deriving over renamed types

[Lennart Augustsson]

Ashley Yakeley wrote:

> At 2002-04-08 12:45, Lennart Augustsson wrote:
>
> >I just just wanted to say that I agree with almost everything Conor said.
> >I find it a little odd that the extension to Haskell that allows explicit
> >forall
> >does not also allow you use explicit type application (and type lanbda).
>
> What did you have in mind?

Actually, what you are proposing was not at all what I was thinking of
(even if I think something like what you propose would be useful).
I was referring to the expression language.

So this is already allowed:
f :: (forall a . a -> a) -> (b, c) -> (c ,b )
f i (x,y) = (i y, i x)

I'd like to be able to have explicit type applications.
If we denote type application with infix # I'd like to write
f i (x, y) = (i#c y, i#b x)

And where you invoke f you could use a type lambda
... f (/\a -> \ x -> (x::a)) ...

It doesn't make much sense in this example, but there are others
where the implcit stuff just doesn't allow you to do what you want.

    -- Lennart


>
>
>   data Zero;
>   data Succ n;
>
>   type Add Zero b = b;
>   type Add (Succ a) b = Succ (Add a b);
>
>   type Mult Zero b = Zero;
>   type Mult (Succ a) b = Add b (Mult a b);
>
>   type Fact Zero = Zero;
>   type Fact (Succ n) = Mult (Succ n) (Fact n);
>
>   data Foo f = MkFoo (f ());
>
>   type Succ' = Succ;
>   type 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 :: (Add (Succ Zero));
>
> --
> Ashley Yakeley, Seattle WA
>
> _______________________________________________
> Haskell mailing list
> Haskell@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell