Using the standard encoding of a free monad in Haskell and its fmap
instance:
data Free f a = Pure a
| Roll (f (Free f a))
Writing an equivalent to this in a dependently typed theory gets rejected because of the strict positivity condition.
Is it possible to cause non-termination with this encoding of a Free
monad?
If this isn't the case does it point to some known relaxation of the strict positivity condition?
If this is the case is there a strictly positive datatype which acts as Free for strictly positive functors?
I don't specify the exact type theory I am working in, as some might allow addition of features to allow this. The base theory might be something like Coq's CoC.
Free
. $\endgroup$ – Labbekak Feb 24 '20 at 7:18Pure a
? $\endgroup$ – András Kovács Feb 25 '20 at 8:08Free
, I'd suggest reading Dylus' 'One Monad To Prove Them All' $\endgroup$ – gallais Feb 27 '20 at 22:02