search

typedefs / typedefs

Programming language agnostic type construction language based on polynomials.
http://typedefs.com/
GNU Affero General Public License v3.0
366 stars 18 forks source link

implement `weakenMu` #190

Closed marcosh closed 4 years ago

marcosh commented 5 years ago

implement a function which allows to drop the context in Mu terms

clayrat commented 5 years ago

To clarify, we need to extend the context instead of dropping it, i.e. a function of (approximate) type Mu [] t -> Mu [...] (weaken t)

clayrat commented 5 years ago

It turns out to be an actual rabbit hole, the problem is that we need a signature like weakenMu : {v : Vect n Type} -> Mu [] t -> Mu v (weakenTDef t (S n) (LTESucc LTEZero)) which means you need to prove all kinds of nasty stuff, e.g. properties of rewrite in the TVar case, and various ways of redistributing weakenTDef internally in recursive cases.

However, if you have a concrete t, you can usually skip that and just reindex your structure naively. Maybe we could have a tactic for generating these weakenings?

andrevidela commented 4 years ago

Is this still needed? Should we prioritise it for Statebox-core?

andrevidela commented 4 years ago

Lets close this for now and re-open it if we run into it again