Why inductive datatypes forbid types like `data Bad a = C (Bad a -> a)` where the type recursion occurs in front of ->?

16
votes

Agda manual on Inductive Data Types and Pattern Matching states:

To ensure normalisation, inductive occurrences must appear in strictly positive positions. For instance, the following datatype is not allowed: 

data Bad : Set where
  bad : (Bad → Bad) → Bad

since there is a negative occurrence of Bad in the argument to the constructor.

Why is this requirement necessary for inductive data types?

2
haskellrecursive-datastructuresalgebraic-data-typesy-combinatoragda

2 Answers

14
votes

The data type you gave is special in that it is an embedding of the untyped lambda calculus.

data Bad : Set where
  bad : (Bad → Bad) → Bad

unbad : Bad → (Bad → Bad)
unbad (bad f) = f

Let's see how. Recall, the untyped lambda calculus has these terms:

 e := x | \x. e | e e'

We can define a translation [[e]] from untyped lambda calculus terms to Agda terms of type Bad (though not in Agda):

[[x]]     = x
[[\x. e]] = bad (\x -> [[e]])
[[e e']]  = unbad [[e]] [[e']]

Now you can use your favorite non-terminating untyped lambda term to produce a non-terminating term of type Bad. For example, we could translate (\x. x x) (\x. x x) to the non-terminating expression of type Bad below:

unbad (bad (\x -> unbad x x)) (bad (\x -> unbad x x))

Although the type happened to be a particularly convenient form for this argument, it can be generalized with a bit of work to any data type with negative occurrences of recursion.

13
votes

An example how such a data type allows us to inhabit any type is given in Turner, D.A. (2004-07-28), Total Functional Programming, sect. 3.1, page 758 in Rule 2: Type recursion must be covariant."

Let's make a more elaborate example using Haskell. We'll start with a "bad" recursive data type

data Bad a = C (Bad a -> a)

and construct the Y combinator from it without any other form of recursion. This means that having such a data type allows us to construct any kind of recursion, or inhabit any type by an infinite recursion.

The Y combinator in the untyped lambda calculus is defined as

Y = λf.(λx.f (x x)) (λx.f (x x))

The key to it is that we apply x to itself in x x. In typed languages this is not directly possible, because there is no valid type x could possibly have. But our Bad data type allows this modulo adding/removing the constructor:

selfApp :: Bad a -> a
selfApp (x@(C x')) = x' x

Taking x :: Bad a, we can unwrap its constructor and apply the function inside to x itself. Once we know how to do this, it's easy to construct the Y combinator:

yc :: (a -> a) -> a
yc f =  let fxx = C (\x -> f (selfApp x))  -- this is the λx.f (x x) part of Y
        in selfApp fxx

Note that neither selfApp nor yc are recursive, there is no recursive call of a function to itself. Recursion appears only in our recursive data type.

We can check that the constructed combinator indeed does what it should. We can make an infinite loop:

loop :: a
loop = yc id

or compute let's say GCD:

gcd' :: Int -> Int -> Int
gcd' = yc gcd0
  where
    gcd0  :: (Int -> Int -> Int) -> (Int -> Int -> Int)
    gcd0 rec a b  | c == 0     = b
                  | otherwise  = rec b c
      where c = a `mod` b