Deducing a type signature

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
3 messages Options
Reply | Threaded
Open this post in threaded view
|

Deducing a type signature

R J-3
Bird 1.6.3 requires deducing type signatures for the functions "strange" and "stranger."

Are my solutions below correct?

(i)  strange f g = g (f g)

Assume g :: a -> b.  Then f :: (a -> b) -> c.  But since g :: a -> b,
f g :: a, so c = a.  Therefore, f :: (a -> b) -> a, and g (f g) :: a.
Therefore, strange :: ((a -> b) -> a) -> (a -> b) -> a.

(ii)  stranger f = f f

Assume f :: a -> b.  Since "f f" is well-typed, type unification requires
a = b.  Therefore, f :: a -> a, and stranger :: (a -> a) -> a.


Hotmail is redefining busy with tools for the New Busy. Get more from your inbox. See how.
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Deducing a type signature

Richard A. O'Keefe

On May 20, 2010, at 11:03 AM, R J wrote:

> stranger f = f f
>

This doesn't have a type in Haskell.
Suppose f :: a -> b
Then if f f made sense, a = (a -> b) would be true,
and we'd have an infinite type.

Type the definition into a file, and try loading it
into ghci:

     Occurs check: cannot construct the infinite type: t = t -> t1
     Probable cause: `f' is applied to too many arguments
     In the expression: f f
     In the definition of `stranger': stranger f = f f

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Deducing a type signature

Dan Weston
In reply to this post by R J-3
 > (i)  strange f g = g (f g)
 >
 > Assume g :: a -> b.  Then f :: (a -> b) -> c.  But since g :: a -> b,
 > f g :: a, so c = a.  Therefore, f :: (a -> b) -> a, and g (f g) :: a.
 > Therefore, strange :: ((a -> b) -> a) -> (a -> b) -> a.

Almost. The return type of strange is the same as the return type of g
(the outermost function), namely b.

So strange :: ((a -> b) -> a) -> (a -> b) -> b.

Dan

R J wrote:

> Bird 1.6.3 requires deducing type signatures for the functions "strange"
> and "stranger."
>
> Are my solutions below correct?
>
> (i)  strange f g = g (f g)
>
> Assume g :: a -> b.  Then f :: (a -> b) -> c.  But since g :: a -> b,
> f g :: a, so c = a.  Therefore, f :: (a -> b) -> a, and g (f g) :: a.
> Therefore, strange :: ((a -> b) -> a) -> (a -> b) -> a.
>
> (ii)  stranger f = f f
>
> Assume f :: a -> b.  Since "f f" is well-typed, type unification requires
> a = b.  Therefore, f :: a -> a, and stranger :: (a -> a) -> a.
>
> ------------------------------------------------------------------------
> Hotmail is redefining busy with tools for the New Busy. Get more from
> your inbox. See how.
> <http://www.windowslive.com/campaign/thenewbusy?ocid=PID28326::T:WLMTAGL:ON:WL:en-US:WM_HMP:042010_2>
>

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe