Path’s type system is closed—datatypes are treated as lambda encodings, and there are no mechanisms to extend the set of available types/values axiomatically. This means that its type system is essentially structural, rather than nominal.
This is a big part of why it’s difficult to pretty-print types nicely (cf #34); there’s nothing playing the role of a constructor (even in some erased form à la newtypes), so we have to embed neutral terms, force them during elaboration, and hope for the best.
It’d be nice to have something corresponding to a newtype which we could use to hang names on a lambda encoding, and other attendant features like typeclasses (cf #49). But it’s not immediately obvious how to do that in a consistently erasable manner, and ideally without opening the theory (i.e. introducing new axioms).
Path’s type system is closed—datatypes are treated as lambda encodings, and there are no mechanisms to extend the set of available types/values axiomatically. This means that its type system is essentially structural, rather than nominal.
This is a big part of why it’s difficult to pretty-print types nicely (cf #34); there’s nothing playing the role of a constructor (even in some erased form à la
newtypes), so we have to embed neutral terms, force them during elaboration, and hope for the best.It’d be nice to have something corresponding to a
newtypewhich we could use to hang names on a lambda encoding, and other attendant features like typeclasses (cf #49). But it’s not immediately obvious how to do that in a consistently erasable manner, and ideally without opening the theory (i.e. introducing new axioms).