haskelltypestype-inferencetype-variables# 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).

Solution

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.

- Comparing lists in Haskell
- Is there a non-identity monad morphism M ~> M that is monadically natural in M?
- Problem with loading module ‘Distribution.Simple’
- Improving efficiency in Stirling numbers calculation
- Does sequencing an infinite list of IO actions by definition result in a never-ending action? Or is there a way to bail out?
- How to call pgQuery from postgresql-query?
- How to avoid whitespace after a tag (link) in Hamlet templates?
- Understanding type-directed resolution in Haskell with existential types
- Why is seq bad?
- Understanding bind function in Haskell
- How to create route that will trigger on any path in Servant?
- How do I use a global state in WAI middleware?
- nixos 23.11 cabal install mysql-simple problem - "Missing (or bad) C libraries"
- Is there a way to kill all forked threads in a GHCi session without restarting it?
- Why can an invalid list expression such as 2:1 be assigned to a variable, but not printed?
- Iterate over a type level list and call a function based on each type in the list
- How does this solution of Project Euler Problem 27 in the Haskell Wiki work?
- Why `Monad` is required to use `pure`?
- Can't do partial function definitions in GHCi
- recommended way to convert Double -> Float in Haskell
- Haskell profiling understanding cost centre summary for anonymous lambda
- Why is Haskell fully declarative?
- GHC Generating Redundant Core Operations
- Question about Event firing in reflex-frp
- Using Haskell's "Maybe", type declarations
- How can I elegantly invert a Map's keys and values?
- Why there is no output for wrapped IO in Haskell?
- What are the definitions of Weather and Memory in xmobar repo?
- Serializing a Data.Text value to a ByteString without unnecessary \NUL bytes
- Using Haskell with VS Code