[Agda] defining coinductive types
Pierre-Evariste Dagand
pedagand at gmail.com
Wed Dec 18 20:02:35 CET 2013
Hi Aaron,
> But I am asking about positive but not strictly positive recursive types.
I believe that the canonical example of such a beast is the functor
T X = (X -> Bool) -> Bool
that, in predicative type theory, does not admit an initial algebra.
That much is said by Altenkirch & Morris in "Indexed containers"
([http://www.cs.nott.ac.uk/~txa/publ/ICont.pdf], p.5).
You might ask 'why?'. So did I. To which Peter Hancock replied with a
reference to Reynolds' "Polymorphism is not set-theoretic", where the
initial algebra of this functor plays a central rôle (bottom of
p.149). An approximate tl;dr of this paper (which should be taken with
a pinch of salt) seems to be that: if you've the initial algebra of
the ill-fated functor T, you cannot have a set theoretic model of your
logic.
For the sake of completeness, I should also mention Pitts'
"Polymorphism is set theoretic, constructively", which I won't dare
comment.
Cheers,
--
Pierre
More information about the Agda
mailing list