tags:

views:

170

answers:

3

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.

+6  A: 

x =::= x x ($) is also true for x = const, which has the type a -> b -> a. So it does not uniquely identify the type.

sepp2k
+1  A: 

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.

sclv
+8  A: 

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.

Carl