Inductive Types

[solomon-b]

No description provided.

[MonoidMusician]

The main question is do we want to implement mu/nu or Free/Cofree. I think we are leaning towards the latter, especially since mu f = Free f 0 and nu f = Cofree f 1.

[dspivak]

I also lean toward the latter, and I would be really happy to have this, especially cofree!

For cofree, you could first implement nu f, and just use it as the base of Cofree f. So it's a step, like P=>Q is a step for computing [P,Q]. Similarly, for Free f, you could first implement mu for arbitrary f, and then use mu (f+1), which is the base of Free f.

[solomon-b]

What about if we implemented so-called nominal inductive types a la https://github.com/solomon-b/lambda-calculus-hs/blob/main/main/08-NominalInductiveTypes.hs

Is this too informal for polytt?