Type theory and fixed points of datatypes

Question

For the purposes of this question, say that a datatype is a type constructor with one type parameter (this is sometimes called a type operator).

In Haskell, we can define a fixed point Fix f of a datatype f by

data Fix f = FixC (f (Fix f)).

For consistency reasons we cannot define a similar fixed point operator of datatypes in dependent type theories (let's say predicative MLTT+infinitely many universes), but we can define fixed points of most datatypes by hand.

Is this the case for all datatypes? i.e. is the issue of getting fixed operator for Set -> Set type families, only that we would then be able to take fixed point of fixed point or is there already a datatype in type theory, where if it had a fixed point the type theory would be inconsistent?

For example it is certainly the case for the wideclass of strictly positive datatypes known as containers, which can according to Containers: Constructing strictly positive types represent all strictly positive types, but each container actually has a fixed point in type theory and there is a fixed point operator in type theory working over containers. Is this reasoning correct? Is the issue just that we can not internally prove that all datatypes are containers cause then we would run into the inconsistency again?

If it's the former, are there type theories where taking fixed point of anything but the fixed point operator itself is allowed, possibly distinguishing it by some modality? Does a satisfying answer (positive or negative) to this appear in literature somewhere?

Edit, attempting to clear up some confusion:

We can not have fix. Is it possible to calculate result of fix of each datatype metatheortically? If so can we add this through modalities? Does the following hold metatheoretically: If MLTT + universes derives, |- T : (Set -> Set), can we always derive some |- TFixP : Set, such that TFixP , T |- T TFixP ≅ TFixP? I suspect no, but failing to construct a countexample. Is there some? For example for id, the fixed point can be constructed by saying data FixId = FixIdC (id FixId) or equivalently data FixId = FixIdC FixId, we are free to say this. It defines an empty type, but defining an empty type is fine.

Edit: Andrej Bauer's answer gives an example of a contravariant type operator f, whose fixed point can not exist. Is there an example of a covariant one? I realized, I was really thinking about covariant type operators, i.e. admitting a law-abiding fmap?

Answer 1

Let a be a type. If there is a type T a which is isomorphic to T a -> a then a has the fixed-point operator, by Lawvere's fixed point theorem. Here is the implementation of such a fixed-point operator in Haskell.

data T a = Wrap (T a -> a)

-- The inverse of T
unwrap :: T a -> (T a -> a)
unwrap (Wrap g) = g

-- Lawvere's fixed-point theorem
fix :: (a -> a) -> a
fix f = unwrap y y
  where y = Wrap (\x -> f (unwrap x x))

-- Example: factorial
fact :: Integer -> Integer
fact = fix (\ f n -> if n == 0 then 1 else n * f (n - 1))

Observe that definition of fix does not use any recursion.

If we could do the above in type theory, then in particular we could prove that every map f : bool → bool has a fixed point, but negation does not. This would allow us to inhabit every type.

Supplemental: We may instantiate the above with a = Bool to obtain the following type-theoretic fact. If there is a type t which is isomorphic to t → bool then the empty type is inhabited. This shows that there are type constructors, namely a ↦ (a → bool) does not have a fixed-point in type theory. So the answer to the question "can we compute the fixed point of every type constructor meta-theoretically?" is "no, because the type constructor a ↦ (a → bool) does not have a fixed point".

Answer 2

If it's the former, are there type theories where taking fixpoint of anything but the fixpoint itself is allowed, possibly distinguishing it by some modality?

This sounds exactly like Guarded Type Theory to me.

The idea is that there's a $\triangleright$ modality, called "later", where $\triangleright T$ denotes a value of type $T$ at some point in the future. $\triangleright$ is an Applicative Functor, but not a monad: we have $next : T \to \triangleright T$ and $app : \triangleright(S \to T) \to \triangleright S \to \triangleright T$.

Critically, we also have Löb Induction: $lob : (\triangleright T \to T) \to T$. That is, we can take the fixed-point of anything, provided that it only refers to itself under the guarded modality. So one can take fixed-points of types, and perform infinite computations, under the guarded modality.

Depending on the flavour of guarded recursion, there are different propositional equalities available to you, along with different constructs. Many allow you to write a type transformer $\blacktriangleright : \triangleright Type \to Type$, which, when combined with $lob$, so you then have $(\lambda F \ldotp lob (\lambda X \ldotp F (\blacktriangleright X))) : (Type \to Type) \to Type$ which lets you take the (guarded) fixed-point of any type function.

If you're at all familiar with step-indexed logical relations, guarded recursion is basically the type-theoretic version of that. Iris, a Coq framework for separation logic, uses Guarded Type Theory to ensure that the user doesn't have to manage step indexing on their own.

Guarded type theory is still an active area of research, and people are exploring various ways to make type-checking decidable, cubical interpretations of equality, etc.

Some reading:

https://bentnib.org/productive.pdf

https://link.springer.com/chapter/10.1007/978-3-662-49630-5_2

https://cs.au.dk/~birke/papers/sgdtuniverse-conf.pdf

https://arxiv.org/pdf/1804.09098.pdf

https://arxiv.org/abs/1606.05223

https://niccoloveltri.github.io/cpp20.pdf

Answer 3

As an aside on top of Andrej Bauer's answer, answering my extended question in edit. To find a strictly positive covariant functor, which does not admit a fixed point, we can look at the Continuation monad.

data Cont r a = Cont ((a -> r) -> r)

This is a functor.

fmap f (Cont x) = Cont (\ z -> x (z ∘ f))

It is easy to check it satisfies the identity and composition laws.

But attempting to take a fixed point results in the following datatype

data FixCont r = FixCont ((FixCont r -> r) -> r), that is not strictly positive. If anyone can derive bottom using this, that would make a nice expansion to this answer, but for now this answers, what I have been trying to derive.

Answer 4

Here is a way to reach inconsistency, via Russell's paradox. Notice that this runs like Andrej's answer, and effectively builds a Y-combinator.

data Fix f = Fix (f (Fix f))

data PreSet a = PreSet (a -> Bool)

type Set = Fix PreSet

test : Set -> Set -> Bool
test (Fix (Preset query)) s = query s

russell : Set
russell = Fix $ Preset \s -> not $ test s s

oops : Bool
oops = test russell russell