(Disclaimer: I'm not 100% sure how codatatype works, especially when not referring to terminal algebras). Consider the "category of types", something like Hask but with whatever adjustmen...

I understand how to define both homogeneous and heterogeneous streams in Haskell. -- Type-invariant streams. data InvStream a where (:::) :: a -> InvStream a -> InvStream a -- Heterogeneous...

In Prolog, is the unification X = [1|X] a sane way to get an infinite list of ones? SWI-Prolog does not have any problem with it, but GNU Prolog simply hangs. I know that in most cases I could rep...

I'm trying to code a functional semantics for IMP language with parallel preemptive scheduling as presented in section 4 of the following paper. I'm using Agda 2.5.2 and Standard library 0.13. Als...

So I've been reading about coinduction a bit lately, and now I'm wondering: are Haskell lists inductive or coinductive? I've also heard that Haskell doesn't distinguish the two, but if so, how do t...

> {-# LANGUAGE DeriveFunctor, Rank2Types, ExistentialQuantification #-} Any inductive type is defined like so > newtype Ind f = Ind {flipinduct :: forall r. (f r -> r) -> r} > ind...