function type def

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

function type def

PR Stanley
HI
It's one of those things - I know sort of instinctively why it is so
but can't think of the formal rationale for it:
f g x = g (g x) :: (t -> t) -> (t -> t)
Why not
(t -> t) -> t -> (t -> t)
to take account of the argument x for g?
Cheers
Paul

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

Re: function type def

Ketil Malde-5
PR Stanley <[hidden email]> writes:

> It's one of those things - I know sort of instinctively why it is so
> but can't think of the formal rationale for it:

> f g x = g (g x) :: (t -> t) -> (t -> t)

(t -> t) -> (t -> t)

So
   g :: t -> t
   x :: t
Thus
   f :: (t -> t) -> t -> t

(The last parenthesis is not necessary, but implies that the type of
the partial application  f g  is a function t -> t .)

-k
--
If I haven't seen further, it is by standing in the footprints of giants
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: function type def

jerzy.karczmarczuk
In reply to this post by PR Stanley
PR Stanley:

> I know sort of instinctively why it is so but
> can't think of the formal rationale for it:
> f g x = g (g x) :: (t -> t) -> (t -> t)

First of all - it is not the definition f g x = ... :: (t-> ...
but the type of the function which might be specified:
f :: (t->t)->t->t

Then, the answer to:
> Why not
> (t -> t) -> t -> (t -> t)
> to take account of the argument x for g?

is simple. If t is the type of x, then g must be g :: t->t, you're right.
So f :: (t->t) -> t -> [the type of the result]
But this result is of the type t, it is g(g x), not (t->t), it is as
simple as that. Perhaps you didn't recognize that "->" is syntactically
a right-associative op, so
a->b->c   is equivalent to a->(b->c), or
(t->t)->t->t         equiv. to  (t->t)->(t->t)


Jerzy Karczmarczuk

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

Re: function type def

PR Stanley
Try putting this through your GHCI:
:t twice f x = f (f x)
I'd presume that based on the inference of (f x) f is (t -> t) and x :: t

Yes, Maybe I should get the right associativity rule cleared first.
Cheers,
Paul

At 20:35 01/04/2008, you wrote:

>PR Stanley:
>>I know sort of instinctively why it is so but can't think of the
>>formal rationale for it:
>>f g x = g (g x) :: (t -> t) -> (t -> t)
>
>First of all - it is not the definition f g x = ... :: (t-> ...
>but the type of the function which might be specified:
>f :: (t->t)->t->t
>Then, the answer to:
>>Why not
>>(t -> t) -> t -> (t -> t)
>>to take account of the argument x for g?
>
>is simple. If t is the type of x, then g must be g :: t->t, you're right.
>So f :: (t->t) -> t -> [the type of the result]
>But this result is of the type t, it is g(g x), not (t->t), it is as
>simple as that. Perhaps you didn't recognize that "->" is syntactically
>a right-associative op, so
>a->b->c   is equivalent to a->(b->c), or
>(t->t)->t->t         equiv. to  (t->t)->(t->t)
>
>Jerzy Karczmarczuk
>_______________________________________________
>Haskell-Cafe mailing list
>[hidden email]
>http://www.haskell.org/mailman/listinfo/haskell-cafe

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