Sometimes, writing Haskell is like having an argument with the compiler. You give it your reasoning, and it checks it over for flaws. And if it thinks it finds one, it will tell you all about it. You then have to look over what it told you, and figure out exactly what its complaint is. *Did I just express myself badly? Or am I actually wrong?* Or, very occasionally, the compiler is just being petulant and you have to work around it. Of course, if you’re *really* upset about GHC not accepting your perfectly reasonably argued program, you can go tell its parents.

Haskell’s type system is pretty great, but one thing it doesn’t have, that some other type systems do have, is *recursive* types, by which I mean, types directly constructed from themselves. Recursive types are forbidden in Haskell.

Let’s say we want to create a recursive type `T = Maybe T`

. The official introductory Haskell answer to this is that one cannot do this directly, but one can easily create a type `T`

that *contains* `Maybe T`

, sometimes called a “newtype wrapper”. Like this:

`newtype T = MkT (Maybe T)`

Simple enough. But can we do better than this? Can we create a type `T`

that is actually equal to `Maybe T`

? *Can we create the forbidden recursive type?*

Let’s start with *won’t* work:

`type T = Maybe T`

Example.hs:6:1: error: Cycle in type synonym declarations: Example.hs:6:1-16: type T = Maybe T

The `type`

keyword creates an *alias* for a type, and aliases cannot be recursive as they must eventually refer to an actual type.

Oddly enough, GHC *does* accept this:

```
type family T where
T = Maybe T
```

Type families are strange things. They’re not quite “real” types, but neither are they mere aliases for types, as they don’t have to be fully resolved. Indeed you can declare a type family in one module, use it all over as if it were a real type, and then define the actual instances of that family in another module.

Sadly, though, GHC won’t let us actually use the instance. It rejects the obvious proof that `T`

and `Maybe T`

are the same type:

```
type family T where
T = Maybe T
proof :: T :~: Maybe T
proof = Refl
```

Example.hs:10:9: error: • Reduction stack overflow; size = 201 When simplifying the following type: T

Why is this? It’s because GHC can’t just accept what it’s been told, and instead endlessly tries to “reduce” (that is, expand) `T = Maybe T = Maybe (Maybe T)`

etc, giving up when it reaches a safety limit. You can think of it as a kind of intellectual black hole, or an “infohazard” for the compiler: if it ever starts examining the strange secrets of your recursive type, it will get lost in the infinite abyss, until a built-in emergency mechanism kicks it awake after it’s twisted in the vortex 200 times (you can change this number if you want, or even let it run forever).

It turns out we *can* construct a type `T`

together with a proper (non-bottom) proof value of `T :~: Maybe T`

, we just have to be discreet. The key is to make sure GHC never comes across the unfathomable constraint `T ~ Maybe T`

, because it will immediately become ensnared in the contemplation of its endlessness.

Instead, we prepare a lemma that is both harmless and more general, and then carefully specialise it to get the terrifying conclusion we want, using the `TypeApplications`

extension, thus avoiding the need for any kind of inference:

```
type family A p q where
A () x = Maybe (A x ())
lemma :: forall x. (A () x) :~: Maybe (A x ())
lemma = Refl
type T = A () ()
proof :: T :~: Maybe T
proof = lemma @()
```

Actually constructing and deconstructing values of `T`

will require a similar circumspection. The trick is, we don’t let GHC infer types. We musn’t let GHC *think*, because thinking about the bad thing leads it to madness. Instead, we apply all types by hand. Here’s the full program, including all the necessary extensions:

```
{-# LANGUAGE RankNTypes, TypeApplications, TypeOperators,
TypeFamilies, UndecidableInstances, AllowAmbiguousTypes #-}
module Main where
import Data.Type.Equality
type family A p q where
A () x = Maybe (A x ())
lemma :: forall x. (A () x) :~: Maybe (A x ())
lemma = Refl
type T = A () ()
proof :: T :~: Maybe T
proof = lemma @()
convert1 :: forall a b. a :~: b -> a -> b
convert1 Refl = id
convert2 :: forall a b. a :~: b -> b -> a
convert2 Refl = id
tconvert1 :: T -> Maybe T
tconvert1 = convert1 @T @(Maybe T) proof
tconvert2 :: Maybe T -> T
tconvert2 = convert2 @T @(Maybe T) proof
nothing :: T
nothing = tconvert2 $ Nothing @T
just :: T -> T
just x = tconvert2 $ Just @T x
count :: T -> Int
count t = case tconvert1 t of
Nothing -> 0
Just t' -> succ $ count t'
t3 :: T
t3 = just $ just $ just nothing
main :: IO ()
main = putStrLn $ show $ count t3
```

This program defines a truly recursive type `T = Maybe T`

, constructs a value of it, and then deconstructs that value. (It does indeed correctly print “3”.) On the other hand, it’s *much* more complicated than just using a newtype like we’re supposed to…

— Ashley Yakeley

Pingback: Forbidden Haskell Types | Hacker News

Pingback: Resumen de lecturas compartidas durante julio de 2020 | Vestigium