Is there a type we can give to y f = f . f y id y head y fst are all typeable? Jim Apple
On Mon, 28 Feb 2005 03:50:14 -0500 Jim Apple <japple@freeshell.org> wrote:
Is there a type we can give to
y f = f . f
y id y head y fst
are all typeable?
Using ghci: Prelude> let y f = f.f Prelude> :t y y :: forall c. (c -> c) -> c -> c So it admits principal type (a->a) -> a->a. From this you can see that (y head) and (y fst) cannot be typed, whereas (y id) can. BTW, this function is usually named 'twice'. Best regards, Pedro -- Pedro Vasconcelos, School of Computer Science, University of St Andrews ----------------------------------------------------------------------- "The difference between Theory and Practice is greater in Practice than in Theory."
The name y suggests that you want to define the fixpoint combinator. This works as follows: Prelude> let y f = f (y f) Prelude> :type y y :: forall t. (t -> t) -> t Prelude> y (\fac n -> if n == 0 then 1 else n*fac(n-1)) 10 3628800 Prelude> Till Pedro Vasconcelos wrote:
On Mon, 28 Feb 2005 03:50:14 -0500 Jim Apple <japple@freeshell.org> wrote:
Is there a type we can give to
y f = f . f
y id y head y fst
are all typeable?
Using ghci:
Prelude> let y f = f.f Prelude> :t y y :: forall c. (c -> c) -> c -> c
So it admits principal type (a->a) -> a->a. From this you can see that (y head) and (y fst) cannot be typed, whereas (y id) can. BTW, this function is usually named 'twice'.
Best regards,
Pedro
-- Till Mossakowski Phone +49-421-218-4683 Dept. of Computer Science Fax +49-421-218-3054 University of Bremen till@tzi.de P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till
Pedro Vasconcelos wrote:
Jim Apple <japple@freeshell.org> wrote:
Is there a type we can give to
y f = f . f
y id y head y fst
are all typeable?
Using ghci:
Prelude> let y f = f.f Prelude> :t y y :: forall c. (c -> c) -> c -> c
So it admits principal type (a->a) -> a->a. From this you can see that (y head) and (y fst) cannot be typed, whereas (y id) can.
I think the OP's point is that all three of his examples make sense, and the resulting functions would have Haskell types, yet there doesn't seem to be a Haskell type which permits all three uses of y. I can come up with types which permit any one of the three: y :: forall a. (a -> a) -> a -> a y :: forall a f. (forall x. f x -> x) -> f (f a) -> a y :: forall a b c f. (forall x y. f x y -> x) -> f (f a b) c -> a but I can't find a type which permits more than one. It can probably be done with type classes. -- Ben
On 2005-02-28 at 18:03GMT Ben Rudiak-Gould wrote:
Pedro Vasconcelos wrote:
Jim Apple <japple@freeshell.org> wrote:
Is there a type we can give to
y f = f . f
y id y head y fst
are all typeable?
Using ghci:
Prelude> let y f = f.f Prelude> :t y y :: forall c. (c -> c) -> c -> c
So it admits principal type (a->a) -> a->a. From this you can see that (y head) and (y fst) cannot be typed, whereas (y id) can.
I think the OP's point is that all three of his examples make sense, and the resulting functions would have Haskell types, yet there doesn't seem to be a Haskell type which permits all three uses of y.
The problem is that the type system needs to be checkable, so has to throw some information away. if y f = f . f, the easiest way of losing information is to require that the output type of f be the same as the input. It certainly needs to be a type acceptable as input to f. if you put th f = f . f . f the examples still make sense, but should the type of th be different from the type of y?
but I can't find a type which permits more than one.
Not in Haskell. 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 Now we can type d id id :: ∀t . t → t so id :: ∀t . (λt.t) t → t ie b is (λt.t) so d id :: (λt.t)((λt.t) t) → t :: ∀t . t → t and d head head:: ∀t.[t]→t so b is [] so d head :: ∀t . [[t]] → t and fst :: ∀x,y.(x,y)→x so b is λx.(x,y) d fst :: ∀t,y . (λx.(x,y))((λx.(x,y)) t) → t :: ∀t,y . (λx.(x,y))(t,y) → t :: ∀t,y . ((t,y),y) → t (oops, only one y) but you would be expecting a bit much of a compiler to infer any of this. -- Jón Fairbairn Jon.Fairbairn at cl.cam.ac.uk
Jon Fairbairn writes:
On 2005-02-28 at 18:03GMT Ben Rudiak-Gould wrote:
Pedro Vasconcelos wrote:
Jim Apple <japple@freeshell.org> wrote:
Is there a type we can give to
y f = f . f
y id y head y fst
are all typeable?
Using ghci:
Prelude> let y f = f.f Prelude> :t y y :: forall c. (c -> c) -> c -> c
So it admits principal type (a->a) -> a->a. From this you can see that (y head) and (y fst) cannot be typed, whereas (y id) can.
I think the OP's point is that all three of his examples make sense, and the resulting functions would have Haskell types, yet there doesn't seem to be a Haskell type which permits all three uses of y.
The problem is that the type system needs to be checkable, so has to throw some information away.
There are type systems which can type this, but they have their own quirks. For example, System E [1] would give us: y :: (a -> b & b -> c) -> a -> c where "a & b" is the intersection of types "a" and "b". The advantage of System E over, say, System F, is that type inferencing is decidable. The downside is that the inferred types can be pretty long. [1] <http://www.macs.hw.ac.uk/~sebc/> -- David Menendez <zednenem@psualum.com> <http://www.eyrie.org/~zednenem/>
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
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.net⑆john⑈
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
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
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
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
Here's a type that fits: d :: forall b a t c. (F t c b, F t a c) => t -> a -> b from the following code:
-# OPTIONS -fglasgow-exts #-} module Main where
main :: IO () main = putStrLn "OK"
data ID = ID data HEAD = HEAD data FST = FST
class F t a b | t a -> b where f :: t -> a -> b instance F ID a a where f _ a = a instance F HEAD [a] a where f _ a = head a instance F FST (a,b) a where f _ a = fst a
d :: (F t a c, F t c b) => t -> a -> b d t = f t . f t
t0 a = d ID a t1 a = d HEAD a t2 a = d FST a
Keean. Jim Apple wrote:
Is there a type we can give to
y f = f . f
y id y head y fst
are all typeable?
Jim Apple
_______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
participants (9)
-
Ben Rudiak-Gould -
David Menendez -
Jacques Carette -
Jim Apple -
John Meacham -
Jon Fairbairn -
Keean Schupke -
Pedro Vasconcelos -
Till Mossakowski