+++
title = "Reflexive Types"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3b3a"]
forwardlinks = ["3b3c"]
zettelid = "3b3b"
+++

Reflexive types are of the nature of taking an argument which is a
function and returning the Inductive type. Some of these are not legal
in Coq, even though they would be legal in Haskell/ML, as they might
produce computations that run forever. This would destroy all the
confidence that one could have in the proof system, as that would mean
that one could produce a proof for any theorem using an infinite loop.
This can be done because proofs are combined with functions. For
example, a reflexive type that takes the type it defines as an argument
could recurse indefinitely, which should not be allowed to be defined.