Return to 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 fixpoint 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 fixpoint 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?

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?

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 fixpoint 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 fixpoint can not exist. Is there a nice example of a covariant one, this made me realize I was really thinking about covariant type operators, i.e. admitting a law-abiding fmap.

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 fixpoint 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 fixpoint 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?

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

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 fixpoint 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 fixpoint can not exist. Is there a nice example of a covariant one, this made me realize I was really thinking about covariant type operators, i.e. admitting a law-abiding fmap.