6
$\begingroup$

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?

$\endgroup$
8
  • $\begingroup$ 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$? $\endgroup$ Dec 3 '21 at 7:06
  • $\begingroup$ 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$. $\endgroup$ Dec 3 '21 at 7:08
  • $\begingroup$ It should be the first case, what I mean is datatype, which in haskell would be, data Fix f = Fix (f (Fix f)). $\endgroup$
    – Nift
    Dec 3 '21 at 8:16
  • $\begingroup$ Is this clearer after the edit? $\endgroup$
    – Nift
    Dec 3 '21 at 8:23
  • 1
    $\begingroup$ I don't think there's a "fixed point of a functor" characterisation of inductive-inductive types. $\endgroup$
    – Labbekak
    Dec 4 '21 at 9:18
3
$\begingroup$

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 C
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 = C (\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".

$\endgroup$
5
  • $\begingroup$ 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. $\endgroup$
    – Nift
    Dec 3 '21 at 20:51
  • $\begingroup$ 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. $\endgroup$ Dec 3 '21 at 21:23
  • $\begingroup$ Is it clearer now? $\endgroup$ Dec 3 '21 at 21:34
  • $\begingroup$ 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? $\endgroup$
    – Nift
    Dec 4 '21 at 2:57
  • 1
    $\begingroup$ 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 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. $\endgroup$ Dec 4 '21 at 10:10
2
$\begingroup$

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

$\endgroup$
0
$\begingroup$

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.

$\endgroup$
0
$\begingroup$

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
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.