Types corresponding to combinatorial families

[byorgey]

It would be cool to have the ability to describe various sorts of combinatorial structures using types, and be able to talk about things like drawing with and without replacement, etc. I have some vague ideas about how to do this but it would require sitting down and doing some serious thinking and design work.

[byorgey]

This might require introducing kinds and kind checking (which we might want to do anyway to allow parameterized type definitions, see #22). The idea would be to have a language for describing functors and then instantiating them with things like WithoutReplacement (Fin 5) or some such. e.g.

((X * X) * Bool) (WithoutReplacement (Fin 5))

would denote triples of two unequal elements from Fin 5 along with a Bool. The need for functors is because once we add modifiers like WithoutReplacement we need to be able to denote its scope explicitly.

[byorgey]

I'm leaving this open because it's still an interesting idea, but at the moment we don't even have Fin types any more, so this is definitely on hold. At any rate it's more of an open research project than a feature request.

[byorgey]

One of the reasons we removed Fin types is because they don't seem as useful without dependent types. For example we would like mod to be able to have a type like Z -> (n : N) -> Fin n. Adding full dependent types is definitely a no go. But recently I started to wonder how bad it would be if we allow type dependency only for natural numbers. Worth considering.