So I was playing around with Haskell today, thinking about autogeneration of function definitions given a type.
For example, the definition of the function
twoply :: (a -> b, a -> c) -> a -> (b, c)
is obvious to me given the type (if I rule out use of undefined :: a
).
So then I came up with the following:
¢ :: a -> (a ->b) -> b
¢ = flip ($)
Which has the interesting property that
(¢) ¢ ($) :: a -> (a -> b) -> b
Which brings me to my question. Given the relation =::=
for "has the same type as", does the statement x =::= x x ($)
uniquely define the type of x
? Must x =::= ¢
, or does there exist another possible type for x
?
I've tried to work backward from x =::= x x ($)
to deduce x :: a -> (a -> b) -> b
, but gotten bogged down.