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.
x =::= x x ($)
is also true for x = const
, which has the type a -> b -> a
. So it does not uniquely identify the type.
I'd just like add that you should look at http://hackage.haskell.org/package/djinn. It can take many type signatures and derive an implementation from them. If there's only one implementation possible for a type that djinn understands, it will produce it.
From the equation above, we can determine some of a type signature for x. X need not have this type, but it needs to at least unify with this type.
$ :: forall a b. (a -> b) -> a -> b
x :: t1 -> ((a -> b) -> a -> b) -> t1
Given that, it should be straightforward to write a multitude of implementations of x.
精彩评论