Re: deriving over renamed types
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? 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
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
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
Hi Lennart wrote:
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.
There's a plentiful supply of good examples arising naturally from higher-hind polymorphism. * -> * is full of functions with good properties (eg being functorial or monadic) which aren't datatype constructors. Haskell's inability to express them and to instantiate type schemes with them is a serious hindrance to the good functional programming practice of identifying and abstracting common structure. Similarly, it's not too hard to find examples where the potential of local `forall' is thwarted by the lack of the corresponding lambda. These examples are already in circulation. Check out... Richard Bird and Ross Paterson: de Bruijn notation as a nested datatype Generalized folds for nested datatypes My own: Faking it and there are plenty more. These papers are too long, because they contain the same program written several times with different types. The abstraction which combines them just isn't available. Worse, multi-parameter classes contribute a second source of `functions from * to *' which just don't fit in with higher-kind polymorphism. Some rationalization would help. Type theory has already addressed lots of these issues. I'm not making these proposals in a vacuum. Type-level abstraction and application, with defaults computed by unification but explicit overriding available is standard practice in several implementations. Further... Ashley wrote:
data Zero; data Succ n;
type Add Zero b = b; type Add (Succ a) b = Succ (Add a b);
...you can write this program with type classes, but much less clearly and directly. They're a good tool, but the wrong tool for this job, and but this job is worth doing well. In that respect, I'd caution against pattern matching over * and higher-kinds, because these kinds are not closed. That's why I argue in favour of datakinds (given that using genuine term-level data would involve a seismic shift in Haskell's static/dynamic divide). But, imagining that Zero and Suc are the constructors of a datakind Nat over which we can write these programs safely...
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 :: Foo (Add (Succ Zero));
...as has already been pointed out, they all have the same eta-long normal form, being Foo (/\n -> Succ n). Machines are good at figuring this stuff out, which is why I like their help when I'm programming. Working with types which contain computations, it's a great help if you can typecheck your code as you go, and ask for (head) normal forms anytime. This stuff doesn't require a leap in the dark. It just takes a bit of borrowing and adaptation. Cheers Conor
participants (4)
-
Ashley Yakeley -
C T McBride -
Lennart Augustsson -
Pixel