<p>Let <code>a</code> be a type. If there is a type <code>T a</code> which is isomorphic to <code>T a -&gt; a</code> then <code>a</code> has the fixed-point operator, by <a href="https://ncatlab.org/nlab/show/Lawvere%27s+fixed+point+theorem" rel="nofollow noreferrer">Lawvere's fixed point theorem</a>. Here is the implementation of such a fixed-point operator in Haskell.</p>
<pre><code>data T a = Wrap (T a -&gt; a)

-- The inverse of T
unwrap :: T a -&gt; (T a -&gt; a)
unwrap (Wrap g) = g

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

-- Example: factorial
fact :: Integer -&gt; Integer
fact = fix (\ f n -&gt; if n == 0 then 1 else n * f (n - 1))
</code></pre>
<p>Observe that definition of <code>fix</code> does <em>not</em> use any recursion.</p>
<p>If we could do the above in type theory, then in particular we could prove that every map <code>f : bool → bool</code> has a fixed point, but negation does not. This would allow us to inhabit every type.</p>
<p><strong>Supplemental:</strong> We may instantiate the above with <code>a = Bool</code> to obtain the following type-theoretic fact. If there is a type <code>t</code> which is isomorphic to <code>t → bool</code> then the empty type is inhabited.
This shows that there are type constructors, namely <code>a ↦ (a → bool)</code> does not have a fixed-point in type theory. So the answer to the question &quot;can we compute the fixed point of every type constructor meta-theoretically?&quot; is &quot;no, because the type constructor <code>a ↦ (a → bool)</code> does not have a fixed point&quot;.</p>

CC BY-SA 4.0
2021-12-03T20:51:52.690Z
I am not certain, which part of my question this is supposed to answer, T is not strictly positive, right? I am asking, whether every type that can be defined in MLTT, actually has a concrete fixed point, even though we can not have generic fixed point operator. T does not break this I will try updating the question so it's clearer.
Ilk
CC BY-SA 4.0
2021-12-03T21:23:28.717Z
`T a` is the fixed point of the operator $F b = b \to a$, which is definable in MLTT. It would be helpful if you stoped saying "fixed point of a type". The correct phrase is "fixed point of a type **operator**", i.e., we are asking which type operators $F : \mathsf{Type} \to \mathsf{Type}$ have fixed points. I am saying that, given any type $A$, if the type operator $F X = (X \to A)$ has a fixed point, then $A$ has a fix-point operator.
Andrej Bauer
CC BY-SA 4.0
2021-12-03T21:34:07.583Z
Is it clearer now?
Andrej Bauer
CC BY-SA 4.0
2021-12-04T02:57:01.457Z
Yes it is clearer, but made me realize I was thinking about the constrained problem where F is a covariant Functor, i.e. has haskell-ish fmap, compared to the F in this example which is contravariant in b. Would there be a similar datatype without a fixed point, if we restrict ourselves to covariant type operators?
Ilk
CC BY-SA 4.0
2021-12-04T10:10:37.650Z
For covariant operators I would venture to say that it is consistent that they all have fixed points. I am saying so because there are categories in which every (covariant) endofunctor has an initial algebra. [This example](https://math.stackexchange.com/questions/3396264/does-there-exist-an-endofunctor-of-the-category-of-countable-sets-that-lacks-an) does not quite cut it, because countable sets are not closed under $\Pi$. I would expect that with a bit of work we can arrange things so that definable functors are nice enough to have initial algebras. Don't take my word for it, though.
Andrej Bauer
CC BY-SA 4.0
2024-10-26T15:56:51.030Z
In the code, two occurrences of `C` should be changed to `T`, yeah?
Hew Wolff
CC BY-SA 4.0
2024-10-26T21:23:07.517Z
Actually, one should be `T` and one should be `Wrap`. Fixed and checked that Haskell likes it. Thanks for pointing it out.
Andrej Bauer
CC BY-SA 4.0
2021-12-03T19:53:49.117Z
2024-10-26T21:22:33.247Z
2024-10-26T21:22:33.247Z
Andrej Bauer
<blockquote>
<p>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?</p>
</blockquote>
<p>This sounds exactly like Guarded Type Theory to me.</p>
<p>The idea is that there's a <span class="math-container">$\triangleright$</span> modality, called &quot;later&quot;, where <span class="math-container">$\triangleright T$</span> denotes a value of type <span class="math-container">$T$</span> at some point in the future. <span class="math-container">$\triangleright$</span> is an Applicative Functor, but not a monad: we have <span class="math-container">$next : T \to \triangleright T$</span> and <span class="math-container">$app : \triangleright(S \to T) \to \triangleright S \to \triangleright T$</span>.</p>
<p>Critically, we also have <em>Löb Induction</em>: <span class="math-container">$lob : (\triangleright T \to T) \to T$</span>. That is, we can take the fixed-point of anything, <em>provided that it only refers to itself under the guarded modality</em>. So one can take fixed-points of types, and perform infinite computations, under the guarded modality.</p>
<p>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 <span class="math-container">$\blacktriangleright : \triangleright Type \to Type$</span>, which, when combined with <span class="math-container">$lob$</span>, so you then have <span class="math-container">$(\lambda F \ldotp lob (\lambda X \ldotp F (\blacktriangleright X))) : (Type \to Type) \to Type$</span> which lets you take the (guarded) fixed-point of any type function.</p>
<p>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.</p>
<p>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.</p>
<p>Some reading:</p>
<p><a href="https://bentnib.org/productive.pdf" rel="nofollow noreferrer">https://bentnib.org/productive.pdf</a></p>
<p><a href="https://link.springer.com/chapter/10.1007/978-3-662-49630-5_2" rel="nofollow noreferrer">https://link.springer.com/chapter/10.1007/978-3-662-49630-5_2</a></p>
<p><a href="https://cs.au.dk/%7Ebirke/papers/sgdtuniverse-conf.pdf" rel="nofollow noreferrer">https://cs.au.dk/~birke/papers/sgdtuniverse-conf.pdf</a></p>
<p><a href="https://arxiv.org/pdf/1804.09098.pdf" rel="nofollow noreferrer">https://arxiv.org/pdf/1804.09098.pdf</a></p>
<p><a href="https://arxiv.org/abs/1606.05223" rel="nofollow noreferrer">https://arxiv.org/abs/1606.05223</a></p>
<p><a href="https://niccoloveltri.github.io/cpp20.pdf" rel="nofollow noreferrer">https://niccoloveltri.github.io/cpp20.pdf</a></p>

CC BY-SA 4.0
2021-12-02T19:51:12.103Z
2021-12-02T22:18:19.217Z
2021-12-02T22:18:19.217Z
Joey Eremondi
<p>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.</p>
<pre><code>data Fix f = Fix (f (Fix f))

data PreSet a = PreSet (a -&gt; Bool)

type Set = Fix PreSet

test : Set -&gt; Set -&gt; Bool
test (Fix (Preset query)) s = query s

russell : Set
russell = Fix <span class="math-container">$ Preset \s -&gt; not $</span> test s s

oops : Bool
oops = test russell russell
</code></pre>

CC BY-SA 4.0
2021-12-09T22:50:34.773Z
2021-12-09T22:50:34.773Z
James Payor
<p>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.</p>
<pre><code>data Cont r a = Cont ((a -&gt; r) -&gt; r)
</code></pre>
<p>This is a functor.</p>
<pre><code>fmap f (Cont x) = Cont (\ z -&gt; x (z ∘ f))
</code></pre>
<p>It is easy to check it satisfies the identity and composition laws.</p>
<p>But attempting to take a fixed point results in the following datatype</p>
<p><code>data FixCont r = FixCont ((FixCont r -&gt; r) -&gt; r)</code>, 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.</p>

CC BY-SA 4.0
2024-07-31T10:18:58.393Z
The recursively defined type `T` such that `T = (T -> r) -> r` is not void, well-defined, and I think one can't derive bottom from having values of that type. (In your notation, `T = FixCont r`. I just consider `r` as a fixed type.) It is not true that the definition of `T` is "not strictly positive" as you say. It is just that `FixCont r` is neither covariant nor contravariant in `r`.
winitzki
CC BY-SA 4.0
2021-12-04T06:04:41.830Z
2021-12-05T13:24:20.503Z
2021-12-05T13:24:20.503Z
Ilk
<p>For the purposes of this question, say that a <strong>datatype</strong> is a type constructor with one type parameter (this is sometimes called a <em>type operator</em>).</p>
<p>In Haskell, we can define a fixed point <code>Fix f</code> of a datatype <code>f</code> by</p>
<pre><code>data Fix f = FixC (f (Fix f)).
</code></pre>
<p>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.</p>
<p>Is this the case for all datatypes? i.e. is the issue of getting fixed operator for <code>Set -&gt; Set</code> 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?</p>
<p>For example it is certainly the case for the wideclass of strictly positive datatypes known as containers, which can according to <a href="http://staff.mmcs.sfedu.ru/%7Eulysses/Edu/SSGEP/uustalu/tcs-containers.pdf" rel="nofollow noreferrer">Containers: Constructing strictly positive types</a> 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?</p>
<p>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?</p>
<p>Edit, attempting to clear up some confusion:</p>
<p>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,  <code>|- T : (Set -&gt; Set)</code>, can we always derive some <code>|- TFixP : Set</code>, such that <code>TFixP , T |- T TFixP ≅ TFixP</code>? 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.</p>
<p>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?</p>

CC BY-SA 4.0
2021-12-03T07:06:14.960Z
What is "the fixpoint of a datatype"? Do you mean a **fixed-point operator**? For example, given a type $T$, this would be $\mathsf{fix} : (T \to T) \to T$ such that $f (\mathsf{fix} \, f) \equiv \mathsf{fix}\, f$ for $f : T \to T$?
Andrej Bauer
CC BY-SA 4.0
2021-12-03T07:08:21.637Z
The other possibility is that you are talking about **fixed points of type constructors**: given a map $F : \mathsf{Set} \to \mathsf{Set}$ you are asking for a type $T$ such that $F(T) \cong T$. If so, do you mean *any* fixed point or an initial one, in which case you should say something about the variance of $F$.
Andrej Bauer
CC BY-SA 4.0
2021-12-03T08:16:09.370Z
It should be the first case, what I mean is datatype, which in haskell would be, data Fix f = Fix (f (Fix f)).
Ilk
CC BY-SA 4.0
2021-12-03T08:23:52.903Z
Is this clearer after the edit?
Ilk
CC BY-SA 4.0
2021-12-03T08:28:56.223Z
So it is a combination of things, namely a fixed-point operator $\mathsf{fix} : (\mathsf{Type} \to \mathsf{Type}) \to \mathsf{Type}$. Yeah, that's too much to ask for.
Andrej Bauer
CC BY-SA 4.0
2021-12-03T15:41:48.190Z
Does the new edit help with clearing up what I am asking? I am not asking about internally having a polymorphic fixed-point operator in the first part. I am asking whether there already is a fixpoint of any concrete type family within the theory.
Ilk
CC BY-SA 4.0
2021-12-03T15:44:59.570Z
Let us [continue this discussion in chat](https://chat.stackexchange.com/rooms/132013/discussion-between-nift-and-andrej-bauer).
Ilk
CC BY-SA 4.0
2021-12-04T09:18:16.477Z
I don't think there's a "fixed point of a functor" characterisation of inductive-inductive types.
Labbekak
<reference-request><type-theory><dependent-type><calculus-of-constructions><fixed-points>
Type theory and fixed points of datatypes
Ilk
# Type theory and fixed points of datatypes

(Asked by: username_0 on 2021-12-02)

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: username_1'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?

**Tags:** reference-request, type-theory, dependent-type, calculus-of-constructions, fixed-points

> **Comments:**
> **username_1**: What is "the fixpoint of a datatype"? Do you mean a **fixed-point operator**? For example, given a type $T$, this would be $\mathsf{fix} : (T \to T) \to T$ such that $f (\mathsf{fix} \, f) \equiv \mathsf{fix}\, f$ for $f : T \to T$?  
> **username_1**: The other possibility is that you are talking about **fixed points of type constructors**: given a map $F : \mathsf{Set} \to \mathsf{Set}$ you are asking for a type $T$ such that $F(T) \cong T$. If so, do you mean *any* fixed point or an initial one, in which case you should say something about the variance of $F$.  
> **username_0**: It should be the first case, what I mean is datatype, which in haskell would be, data Fix f = Fix (f (Fix f)).  
> **username_0**: Is this clearer after the edit?  
> **username_1**: So it is a combination of things, namely a fixed-point operator $\mathsf{fix} : (\mathsf{Type} \to \mathsf{Type}) \to \mathsf{Type}$. Yeah, that's too much to ask for.  
> **username_0**: Does the new edit help with clearing up what I am asking? I am not asking about internally having a polymorphic fixed-point operator in the first part. I am asking whether there already is a fixpoint of any concrete type family within the theory.  
> **username_0**: Let us [continue this discussion in chat](https://chat.stackexchange.com/rooms/132013/discussion-between-nift-and-andrej-bauer).  
> **username_2**: I don't think there's a "fixed point of a functor" characterisation of inductive-inductive types.  

---

## 4 answers

### Answer by username_1 on 2021-12-03. Score: 3 | Accepted answer

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".

> **Comments:**
> **username_0**: I am not certain, which part of my question this is supposed to answer, T is not strictly positive, right? I am asking, whether every type that can be defined in MLTT, actually has a concrete fixed point, even though we can not have generic fixed point operator. T does not break this I will try updating the question so it's clearer.  
> **username_1**: `T a` is the fixed point of the operator $F b = b \to a$, which is definable in MLTT. It would be helpful if you stoped saying "fixed point of a type". The correct phrase is "fixed point of a type **operator**", i.e., we are asking which type operators $F : \mathsf{Type} \to \mathsf{Type}$ have fixed points. I am saying that, given any type $A$, if the type operator $F X = (X \to A)$ has a fixed point, then $A$ has a fix-point operator.  
> **username_1**: Is it clearer now?  
> **username_0**: Yes it is clearer, but made me realize I was thinking about the constrained problem where F is a covariant Functor, i.e. has haskell-ish fmap, compared to the F in this example which is contravariant in b. Would there be a similar datatype without a fixed point, if we restrict ourselves to covariant type operators?  
> **username_1**: For covariant operators I would venture to say that it is consistent that they all have fixed points. I am saying so because there are categories in which every (covariant) endofunctor has an initial algebra. [This example](https://math.stackexchange.com/questions/3396264/does-there-exist-an-endofunctor-of-the-category-of-countable-sets-that-lacks-an) does not quite cut it, because countable sets are not closed under $\Pi$. I would expect that with a bit of work we can arrange things so that definable functors are nice enough to have initial algebras. Don't take my word for it, though.  
> **username_3**: In the code, two occurrences of `C` should be changed to `T`, yeah?  
> **username_1**: Actually, one should be `T` and one should be `Wrap`. Fixed and checked that Haskell likes it. Thanks for pointing it out.  

---

### Answer by username_4 on 2021-12-02. Score: 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://cs.au.dk/%7Ebirke/papers/sgdtuniverse-conf.pdf)

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

<https://arxiv.org/abs/1606.05223>

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


---

### Answer by username_5 on 2021-12-09. Score: 0

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


---

### Answer by username_0 on 2021-12-04. Score: 0

As an aside on top of username_1'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.

> **Comments:**
> **username_6**: The recursively defined type `T` such that `T = (T -> r) -> r` is not void, well-defined, and I think one can't derive bottom from having values of that type. (In your notation, `T = FixCont r`. I just consider `r` as a fixed type.) It is not true that the definition of `T` is "not strictly positive" as you say. It is just that `FixCont r` is neither covariant nor contravariant in `r`.  

---

