search

Andromedans / andromeda

A proof assistant for general type theories
http://www.andromeda-prover.org/
Other
297 stars 34 forks source link

The type of abstraction #485

Open andrejbauer opened 4 years ago

andrejbauer commented 4 years ago

This is a partial response to #482.

The abstraction notation {x : A} C is overloaded, as it has two possible types: C could be a judgement or a boundary. As far as the AML type system is concerned this is a hack (because the only form of polymorphism expressible is parametric polymorphism).

The principled solution would be to introduce several kinds of types. We would have the kind of all types type and the subkind judgement_or_boundary (where of course we'd need a better name). SML uses this solution to keep track of which types have a pre-defined structural equality (the types of kind eqtype).

Once we have the kind of "abstractable types" (so let us call this kind abstype), we would be tempted to stick in it other types, apart from judgement and boundary. For instance, it may be quite useful to have an abstracted pair of judgements, so abstype should/could be closed under products, so that once can have {x : A} (C1, C2) (here C1 and C2 are simultaneously abstracted by x : A). In fact, it could be closed under any type constructor which allows us to "fold" over the type.

It is not quite clear how to design this sort of thing. Does the nucleus know about abstracted pairs of judgements? List of abstacted judgement?

andrejbauer commented 4 years ago

Whether it is worth having things like {x : A} (C1, C2) depends on whether in proof development one ever wants to have a pair of judgements which share a common abstraction. I imagine this sort of thing shows up.