Re: [Haskell] Re: Type of y f = f . f
On Mon, Feb 28, 2005 at 11:10:40PM -0500, 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 Or one could do its dual (?). d :: (forall c . c - b c) - a - b (b a) d f = f . f rank-n polymorphism is fun :) now, I guess the tricky thing is creating a function which will work as d head and d (:[]) ... John -- John Meacham - repetae.netjohn ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
RE: [Haskell] Re: Type of y f = f . f
It is really too bad the 'middle' version does not work, ie John Fairbarn's version d1 :: (forall c . b c - c) - b (b a) - a d1 f = f . f John Meacham's version (dual (?)) d2 :: (forall c . c - b c) - a - b (b a) d2 f = f . f Or something in the middle d3 :: forall e a b . (forall c . e c - b c) - (e a) - (b a) d3 f = f . f but ghci -fglasgow-exts does not like it :-( Jacques ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] Re: Type of y f = f . f
Actually none of these seem to work:
{-# OPTIONS -fglasgow-exts #-}
module Main where
main :: IO ()
main = putStrLn OK
d :: (forall c . b c - c) - b (b a) - a
d f = f . f
t0 = d id
t1 = d head
t2 = d fst
Load this into GHCI and you get:
Test.hs:11:7:
Couldn't match the rigid variable `c' against `b c'
`c' is bound by the polymorphic type `forall c. b c - c' at
Test.hs:11:5-8
Expected type: b c - c
Inferred type: b c - b c
In the first argument of `d', namely `id'
In the definition of `t0': t0 = d id
Test.hs:13:5:
Inferred type is less polymorphic than expected
Quantified type variable `c' escapes
It is mentioned in the environment:
t2 :: (c, (c, a)) - a (bound at Test.hs:13:0)
In the first argument of `d', namely `fst'
In the definition of `t2': t2 = d fst
Failed, modules loaded: none.
Keean.
Jacques Carette wrote:
It is really too bad the 'middle' version does not work, ie
John Fairbarn's version
d1 :: (forall c . b c - c) - b (b a) - a
d1 f = f . f
John Meacham's version (dual (?))
d2 :: (forall c . c - b c) - a - b (b a)
d2 f = f . f
Or something in the middle
d3 :: forall e a b . (forall c . e c - b c) - (e a) - (b a)
d3 f = f . f
but ghci -fglasgow-exts does not like it :-(
Jacques
___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] Re: Type of y f = f . f
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). -- Jn Fairbairn Jon.Fairbairn at cl.cam.ac.uk ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell] Re: Type of y f = f . f
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. Oh, that's bad. 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. This part I don't understand - isn't b anything in *-*? Can't b be the identity functor? Jim ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell] Re: Type of y f = f . f
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 Jim ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
