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 _______________________________________________ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell