On 2005-02-28 at 23:10EST Jim Apple wrote: > Jon Fairbairn wrote: > > If you allow quantification over higher > > kinds, you can do something like this: > > > > d f = f . f > > > > d:: âa::*, b::*â*.(b a â a) â b (b a)â a > > > > What's the problem with > > d :: (forall c . b c -> c) -> b (b a) -> a > d f = f . f > > to which ghci gives the type > > d :: forall a b. (forall c. b c -> c) -> b (b a) -> a
It's too restrictive: it requires that the argument to d be polymorphic, so if f:: [Int]->[Int], d f won't typecheck. It also requires that the type of f have an application on the lhs, so f :: Int->Int won't allow d f to typecheck either. In the imaginary typesystem I was thinking of above, we could instantiate b with (Îx.x). As others have pointed out, there are other typesystems that allow different types that also work. Incidentally, I think Ponder would have assigned types to the examples, just not very useful ones; d head would have come out as (Ît.[t])->(Ît.[t]) (assuming anything came out at all). -- JÃn Fairbairn Jon.Fairbairn at cl.cam.ac.uk _______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
