1

I would like to define the following function:

f a = f

This function takes one argument and returns itself ignoring the argument. Just writing it like this in ghci gives me the following type error:

• Couldn't match expected type ‘t’ with actual type ‘p0 -> t’
   ‘t’ is a rigid type variable bound by
    the inferred type of f :: t

If the function would use this argument it would be possible (as in this halt example):

halt = halt

or with one parameter

halt x = halt x

Would it somehow be possible to name this type or compile the former program? Of course, this is not for any specific reason, just trying to understand type theory, specifically in haskell, better - you could never apply this function enough to yield a specific result.

leo848
  • 637
  • 2
  • 7
  • 24
  • 6
    Here's a mental exercise: what would be the type of such function? – Fyodor Soikin Oct 22 '22 at 16:34
  • I suppose it is a function that accepts an infinite amount of differently typed arguments, like `a -> b -> c -> d -> ...`. I was asking if there could be some sort of syntax for this in haskell or more generelly in type theory, as it is very well possible to write this sort of function in dynamically typed languages like python: `def a(b): return a`. – leo848 Oct 22 '22 at 16:39
  • 1
    Have a look at [How does Haskell printf work?](https://stackoverflow.com/q/7828072/1048572) for handling of variadic arguments. Probably even simpler in your case since the function never needs to actually return anything useful. – Bergi Oct 22 '22 at 17:58
  • This was [recently asked](https://stackoverflow.com/questions/74117157/make-a-function-return-itself-after-doing-some-work) regarding OCaml, and while possible, it was generally regarded as a [questionable idea](https://stackoverflow.com/a/74144408/15261315). – Chris Oct 22 '22 at 23:57

1 Answers1

4

Well, you can "almost" have that.

As already mentioned, you can't have an infinite type like a -> b -> c -> ..., since Haskell types must be finite.

However, we can define a recursive newtype which is "morally" the infinite type above, and use that:

newtype F = F { unF :: forall a. a -> F }

f :: F
f = F (\x -> f)

In simpler terms, this constructs a type F satisfying F ~= forall a . a -> F which is the equation giving rise to the wanted "infinite" type.

Note the use of the forall a to allow x to have any type at all. The (almost-)function f is essentially a "hungry" function that will eat any argument, of any type, and return itself.

There is a downside, though, to this approach. To actually apply f, we need to unwrap the constructor. This leads to code like

g :: F
g = unF (unF f True) "hello"

which is a bit more inconvenient than g = f True "hello".

chi
  • 111,837
  • 3
  • 133
  • 218