mmontin / libndt Goto Github PK

According to @cathdubois, the property

map (fun x => x) xs = xs

is not provable by mere induction for xs an LNDT. Why is that?

References with nested types:

• Okasaki chapter 6
• Hinze's Numerical Representations as Higher-Order Nested Datatypes
• Hinze's Manufacturing datatypes

References in type theory:

• Ko's Binomial heaps
• Swierstra's Heterogeneous binary random-access lists

We need to gain some genericity in the newest versions of our work. There are two options:

• either go back to setw, but that's questionable whether or not that's even possible
• or just use and additional level parameters spread throughout the library

We need to incorporate the automated generation for LNDTs using QuickChick in the Coq side

We need to instantiate GNDT with a higher degree and deduced the iterative counterpart. The ultimate goal would be to have a function that builds the iterative version of any GNDT.

We need to import the branches from PE pull requests to work on them here until they are ready to be merged.

The GNDT definition is unlikely to work in Coq and, at any rate, it won't be convenient.

Instead, one should define type-classes that streamline the necessary code generation process.

We want to make an instantiation of BushTrees as GNDT.