Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Haskell: example of function of type a -> a, besides the identity

I've just started playing a little with Haskell... I want to write a function of the same type of the identity. Obviously, not equivalent to it. That would be something like,

myfunction :: a -> a

I cannot come up with an example in which the parameter and the return type are the same and can be virtually anything (this excludes the possibility of using Haskell's Typeclasses).

like image 997
acrespo Avatar asked Sep 01 '12 19:09

acrespo


People also ask

What does A -> B mean in Haskell?

a -> b Bool means... forall (a :: *) (b :: * -> *). a -> b Bool. b is therefore a type constructor taking a single type argument. Examples of single-argument type constructors abound: Maybe , [] , IO are all examples of things which you could use to instantiate b .

What are high order functions in Haskell?

Haskell functions can take functions as parameters and return functions as return values. A function that does either of those is called a higher order function. Higher order functions aren't just a part of the Haskell experience, they pretty much are the Haskell experience.

What does ID function do Haskell?

id , the identity function, is a function with type a -> a that returns its argument unchanged. const takes two arguments, discards the second and returns the first.

What does == mean in Haskell?

The == is an operator for comparing if two things are equal. It is quite normal haskell function with type "Eq a => a -> a -> Bool". The type tells that it works on every type of a value that implements Eq typeclass, so it is kind of overloaded.

What are the different types of data in Haskell?

An introduction to types, lambda functions and type classes in Haskell, the increasingly popular functional programming language. Ordinary data types are for primitive data (like (Int) and (Char)) and basic data structures (like ( [Int]) and ( [Char])). Functions have types containing an arrow, e.g. (Int rightarrow String).

What is function composition in Haskell?

Haskell - Function Composition. In mathematics, composition is denoted by f {g (x)} where g () is a function and its output in used as an input of another function, that is, f (). Function composition can be implemented using any two functions, provided the output type of one function matches with the input type of the second function.

What is the difference between type and Newtype in Haskell?

Type and newtype. The other two ways one may introduce types to Haskell programs are via the type and newtype statements. type introduces a synonym for a type and uses the same data constructors. newtype introduces a renaming of a type and requires you to provide new constructors.

What is string in Haskell?

Haskell string is a data type which is used to store the value of variable in the form of string, string is represented by the sequence of character in Haskell or in any other programming language as well. String in Haskell provide different functions to manipulate the value of string object, or to perform any operation on it.


5 Answers

This is impossible without using undefined as another commenter mentioned. Let's prove it by counter-example. Assume there were such a function:

f :: a -> a

When you say that's it not the same as id, that implies that you cannot define:

f x = x

However, consider the case where a is the type ():

f () = ...

The only possible result f could return would be (), but that would be the same implementation as id, therefore a contradiction.

The more sophisticated and rigorous answer is to show that the type a -> a must be isomorphic to (). When we say two types a and b are isomorphic, that means that we can define two functions:

fw :: a -> b
bw :: b -> a

... such that:

fw . bw = id
bw . fw = id

We can easily do this when the first type is a -> a and the second type is ():

fw :: (forall a . a -> a) -> ()
fw f = f ()

bw :: () -> (forall a . a -> a)
bw () x = x

We can then prove that:

fw . bw
= \() -> fw (bw ())
= \() -> fw (\x -> x)
= \() -> (\x -> x) ()
= \() -> ()
= id

bw . fw
= \f -> bw (fw f)
-- For this to type-check, the type of (fw f) must be ()
-- Therefore, f must be `id`
= \f -> id
= \f -> f
= id

When you prove two types are isomorphic, one thing you know is that if one type is inhabited by a finite number of elements, so must the other one. Since the type () is inhabited by exactly one value:

data () = ()

That means that the type (forall a . a -> a) must also be inhabited by exactly one value, which just so happens to be the implementation for id.

Edit: Some people have commented that the proof of the isomorphism is not sufficiently rigorous, so I'll invoke the Yoneda lemma, which when translated into Haskell, says that for any functor f:

(forall b . (a -> b) -> f b) ~ f a

Where ~ means that (forall b . (a -> b) -> f b) is isomorphic to f a. If you choose the Identity functor, this simplifies to:

(forall b . (a -> b) -> b) ~ a

... and if you choose a = (), this further simplifies to:

(forall b . (() -> b) -> b) ~ ()

You can easily prove that () -> b is isomorphic to b:

fw :: (() -> b) -> b
fw f = f ()

bw :: b -> (() -> b)
bw b = \() -> b

fw . bw
= \b -> fw (bw b)
= \b -> fw (\() -> b)
= \b -> (\() -> b) ()
= \b -> b
= id

bw . fw
= \f -> bw (fw f)
= \f -> bw (f ())
= \f -> \() -> f ()
= \f -> f
= id

So we can then use that to finally specialize the Yoneda isomorphism to:

(forall b . b -> b) ~ ()

Which says that any function of type forall b . b -> b is isomorphic to (). The Yoneda lemma provides the rigor that my proof was missing.

like image 192
Gabriella Gonzalez Avatar answered Oct 05 '22 23:10

Gabriella Gonzalez


Let me formulate an answer that elaborates on dbaupp’s comment. Any function of type a -> a would also give rise to an function of type () -> (), so I will look at this subproblem first.

A usual semantics of Haskell types and functions would represent a type as a pointed chain-complete partial order, and functions as continuous functions. The type () is represented by the two element set {⊥,()} with the order ⊥⊏(). In plain set theory, there are 2^2=4 functions from this set onto itself, but only three of them are continuous:

  • f1: ⊥ ↦ ⊥, () ↦ ⊥,
  • f2: ⊥ ↦ ⊥, () ↦ (), and
  • f3: ⊥ ↦ (), () ↦ ().

So in our semantic model, there are three different functions of type () -> (). But which of them can be implemented in Haskell? All of them!

  • f1 _ = undefined (or f1 x = f1 x)
  • f2 x = x (or f2 = id)
  • f3 _ = () (or f3 = const ())

Looking at these definitions, you can see that f1 and f2 can also be used to define a function of type a -> a. As they do different things already on (), they are different. So we have at least two different functions of type a -> a.

In the above semantic model, there are many more functions of type a -> a, but these would not be expressible in Haskell (this is related to parametricity and Wadler’s Theorems for Free). A proper proof that f1 and f2 are the only such functions does not seem to be very easy, as it depends on what the Haskell language disallows (e.g. no pattern matching on the type of the argument).

like image 33
Joachim Breitner Avatar answered Oct 05 '22 23:10

Joachim Breitner


Unless you are willing to use undefined or bottom (a non-terminating expression), there literally are no other functions that satisfy that type.

This is one of the large strengths of the Haskell type system. It's possible to strongly limit possible functions that can pass trough a compiler into the ones that are obviously correct. For an extreme example, see djinn -- it takes a type, and generates possible functions that match that type. Even for real, complex examples, the list is often very short.

like image 40
Tuna-Fish Avatar answered Oct 06 '22 00:10

Tuna-Fish


The key here is to understand that we know nothing about a, especially we have no way to generate a new one or to transform it to something different. Hence we have no choice as returning it (or the bottom value). As soon as we have more information about a (e.g. a context bound), we can do more interesting things with it:

f :: Monoid a => a -> a
f _ = mempty

or

f :: Monoid a => a -> a
f x = x `mappend` x `mappend` x

Or if you have the choice like in f :: (a, a) -> a, you have two possible implementations (ignoring the bottom values again), but for f :: (a, b) -> a you are back to one implementation, which is the same as for fst: While it is valid to call f with a pair of identical types, e.g. f ("x", "y"), you can be sure that f behaves like fst, because in the implementation of f you have no way to test if both argument types might be the same. Similarly, there is only one non-bottom version of f :: (a -> b) -> a -> b.

Polymorphism limits the degrees of freedom, because you don't know anything about your arguments, and in some cases it boils down to one non-bottom version.

like image 37
Landei Avatar answered Oct 05 '22 23:10

Landei


As others mentioned, no such other total function can exist. (If we don't limit ourselves to total functions then we can inhabit any type by undefined.)

I'll try to give a theoretical explanation based on the λ-calculus:

For simplicity, let's limit ourselves to λ-terms (to which we can translate any Haskell expression). For a λ-term M let's call A its head if M ≡ A N1 ... Nk and A isn't an application (k can be also zero). Note that if M is in normal form then A cannot be a λ-abstraction unless k = 0.

So let M :: a -> a be a λ-term in normal form. Since we have no variables in the context, M cannot be a variable and it cannot be an application. If it were, its head would have to be a variable. So M must be a λ-abstraction, it must be M ≡ λ(x:a).N.

Now N must be of type a, formally {x:a}⊢N:a. If N was a λ-abstraction, its type would be σ -> τ, which is not possible. If N was a function application then it's head would have to be a variable, and the only one we have in the context is x. But since x:a, we cannot apply x to anything, x P isn't tapeable for any P. So the only possibility is that N ≡ x. So, M must be λ(x:a).x.

(Please correct my English, if possible. In particular, I'm not sure how to use the subjunctive right).

like image 36
Petr Avatar answered Oct 06 '22 01:10

Petr