Istari

Bar (partial types)

Inspired by the partial types (“bar types”) of Constable and Smith [1], but weaker, because we cannot implement the termination predicate.

Pause is just the identity, but we insert it in various places to break up redices so that accidental ill-typed terms don’t result in runaway reduction:

pause : intersect (i : level) (a : U i) . a -> a
      = fn v0 . v0

The general Y combinator is not well typed (if it were, every proposition would be provable), but it can be made type correct using the future modality:

ffix : intersect (i : level) (a : U i) . (future a -> a) -> a
     = fn f .
          pause
            (fn x . f (let next x' = x in next (pause x' x)))
            (next (fn x . f (let next x' = x in next (pause x' x))))

The reduction for ffix is:

ffix f --> f (next (ffix f))

It appears in the registry under the name Bar.unroll_ffix. It can also be used through the unroll tactic.

The partial type bar A provides an A now, or sometime later:

bar : intersect (i : level) . U i -> U i
    = fn a . rec t . a % future t

bar_unroll : forall (i : level) (a : U i) . bar a = (a % future (bar a)) : type

The partial type acts as a monad. Its unit is now:

now : intersect (i : level) (a : U i) . a -> bar a
    = fn x . inl x

Another intro form is laterf:

laterf : intersect (i : level) (a : U i) . future (bar a) -> bar a
       = fn x . inr x

The laterf form is very often used with next, so we define:

later : intersect (i : level) (a : U i) . bar a -> bar a
      = fn x . laterf (next x)

The monadic bind is bindbar:

bindbar : intersect (i : level) (a b : U i) . bar a -> (a -> bar b) -> bar b

bindbar (now x) f --> f x ;
bindbar (laterf x) f --> let next y = x in later (`bindbar y f)
bindbar (later x) f --> later (`bindbar x f)

The syntactic sugar bindbar x = m in n is accepted for `bindbar m (fn x . n).

Observe that bindbar always produces an element of some bar type. A variation on it, bindbart, produces a type instead:

bindbart : intersect (i : level) (a : U i) . bar a -> (a -> U i) -> U i

bindbart (now x) b --> b x ;
bindbart (laterf x) b --> let next y = x in future (`bindbart y b) ;
bindbart (later x) b --> future (`bindbart x b) ;

The syntactic sugar bindbart x = m in b is accepted for `bindbart m (fn x . b).

Bar is covariant:

bar_subtype : forall (i : level) (a b : U i) . a <: b -> bar a <: bar b

Finally we can define a fixpoint operator on partial objects:

bfix : intersect (i : level) (a : U i) . (bar a -> bar a) -> bar a
     = fn f . ffix (fn x . f (laterf x))

The reduction for bfix is:

bfix f --> f (later (bfix f))

It appears in the registry under the name Bar.unroll_bfix. It can also be used through the unroll tactic.

At this point we’d like to follow the development in Smith [2] and define a termination predicate. Alas, we cannot. Istari’s step-indexed semantics is unable to express liveness properties such as termination. If it could express termination, we would be able to draw a contradiction, because the type of bfix does not have Smith’s admissibility requirement. (See Smith [2], theorem 60.)

We can iterate over partial objects using the bar_iter iterator. The cases are now and later:

bar_iter : intersect (i : level) (a : U i) .
              forall (P : bar a -> U i) .
                (forall (x : a) . P (now x))
                -> (forall (xf : future (bar a)) .
                      let next x = xf in future (P x) -> P (later x))
                -> forall (x : bar a) . P x

bar_iter _ hn _ (now x) --> hn x
bar_iter P hn hl (laterf x) --> let next y = x in hl (next y) (next (bar_iter P hn hl y))
bar_iter P hn hl (later x) --> hl (next x) (next (bar_iter P hn hl x))

This is employed automatically by the induction tactic on hypotheses of bar type.


[1] Robert L. Constable and Scott Fraser Smith. Partial Objects in Constructive Type Theory. In Second IEEE Symposium on Logic on Computer Science, 1987.

[2] Scott Fraser Smith. Partial Objects in Type Theory, 1988.