Function Type Calculation (Take 2)
In case you missed it the first time here is my query again: Hi I know we've already looked at the topic of function type calculation though last time I didn't have the chance to go through it thoroughly. So here it is again. Apologies for the repetition. I've had a try at calculating function types for two examples below. So to start with I'd be grateful for an assessment of my efforts. All comments are welcome. Thanks, Paul [1] funk f x = f (funk f) x f :: a x :: b funk f x :: c therefore funk :: a -> b -> c RHS f (funk f) x :: c f (funk f) :: d -> c x :: d f :: e -> d -> c funk :: h -> e f :: h unification f :: a = h = (e -> d -> c) x b = d therefore funk :: ((h -> e) -> b -> c) -> b -> c [2] w f = f f Assigning Types f :: a w f :: b therefore w :: a -> b RHS f f :: b f :: c -> b f :: c f :: a = b = c = (c -> b) therefore w :: (a -> a) -> a
[1] funk f x = f (funk f) x
f :: a x :: b funk f x :: c therefore funk :: a -> b -> c
RHS f (funk f) x :: c
f (funk f) :: d -> c x :: d
f :: e -> d -> c
funk :: h -> e f :: h
unification f :: a = h = (e -> d -> c) x b = d
No. x :: b = d (a typo?) Don't forget also that funk :: a -> b -> c = h -> e, which means that e = b -> c
therefore funk :: ((h -> e) -> b -> c) -> b -> c
No. I don't understand where you've got this expression from. It's funk :: a -> b -> c = (e -> d -> c) -> b -> c = ((b -> c) -> b -> c) -
b -> c
According to GHCi: Prelude> let funk f x = f (funk f) x Prelude> :t funk funk :: ((t1 -> t) -> t1 -> t) -> t1 -> t which is about the same.
[2] w f = f f
Can't be typed in Haskell.
Assigning Types f :: a w f :: b therefore w :: a -> b
RHS f f :: b
f :: c -> b f :: c
f :: a = b = c = (c -> b)
And that's why. It can't happen that c = c -> b. Ever. Prelude> let w f = f f <interactive>:1:10: Occurs check: cannot construct the infinite type: t = t -> t1
[1] funk f x = f (funk f) x f :: a x :: b funk f x :: c therefore funk :: a -> b -> c RHS f (funk f) x :: c f (funk f) :: d -> c x :: d f :: e -> d -> c funk :: h -> e f :: h unification f :: a = h = (e -> d -> c) x b = d No. x :: b = d (a typo?) Paul: What's wrong with x being of type b and of type d? Could you perhaps explain the error please? Don't forget also that funk :: a -> b -> c = h -> e, which means that e = b -> c Paul: is that something to do with partial application? (funk f) is a partially applied function, correct? Again an explanation would be appreciated. therefore funk :: ((h -> e) -> b -> c) -> b -> c No. I don't understand where you've got this expression from. It's funk :: a -> b -> c = (e -> d -> c) -> b -> c = ((b -> c) -> b -> c) - > b -> c According to GHCi: Prelude> let funk f x = f (funk f) x Prelude> :t funk funk :: ((t1 -> t) -> t1 -> t) -> t1 -> t which is about the same. Thanks Paul
participants (2)
-
Miguel Mitrofanov -
PR Stanley