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?
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.
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
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With