I’ve just created Term.lhs. I’ll be filling it up with glue very shortly.

4 Responses to “Term.lhs”

  1. Conor Says:

    I’ve hacked up the basics of the operational behaviour. Next up, a wee parser and printer, so we can have a bit of a play.

  2. Conor Says:

    Module TermParser now contains a highly incomplete parser for fully elaborated raw terms, extracting them as a subset of the concrete syntax, given a resolver for names. You can try it out in ghci thus:

    *TermParser> testTermParser
    all _X : * => all x : X => X
    B (All,Impl) (R *) (Sc (B (All,Expl) (V 0) (Sc (V 1))))

  3. pwm Says:

    Sorry Conor I added code tags to that comment, feel free to reverse this :)

  4. Conor Says:

    More excitement!

    *TermParser> testTermParser
    (λ X : * ⇒ (λ x : X ⇒ (λ y : X ⇒ *) x)) * : ∀ x : * ⇒ *
    Term = E (B (Lam,Expl) (R TT.*) (Sc (B (Lam,Expl) (V 0) (Sc (E (B (Lam,Expl) (V 1) (Sc (R TT.*))) (A (V 0))))))) (A (R TT.*))
    Whnf = B (Lam,Expl) (R TT.*) (Sc (E (B (Lam,Expl) (R TT.*) (Sc (R TT.*))) (A (V 0))))
    Norm = B (Lam,Expl) (R TT.*) (Vac (R TT.*))
    Type = B (All,Expl) (R TT.*) (Sc (R TT.*))

    The test routine now takes term : type. It’s your responsibility to be accurate, as there’s no checker yet. You get back the Haskell show of the term, its whnf, its normal form and the type you supplied. The type is necessary (in general) for the quotation operation. Quotation of Whnv to get a whnf is very cheap, as it’s only skin deep. Quotation of normal forms requires a deeper traversal, and a name supply. However, a little inspired by the ∇-ists, I knocked up this little gadget

    nu :: (IKnow i FreshRoot, Abstract t s) ⇒
      Value → (Value → i t) → i s
    nu ty f = iknow $ λ (FreshRoot (nom, i)) →
      let noo = (nom /. ("x", i)) := Purple ty
      in iI (noo ) (iknew (FreshRoot (nom, i + 1))
       (f (vR noo))) Ii

    nu’s type is more informative, on the face of it: working in any idiom with a name supply, nu ty f gives you the scope-like thing made by abstracting x from (f x) where x is a fresh variable of type ty. Though I say so myself, the nice thing is that the new free variable doesn’t leak: by the time it reaches the outside world, it’s been bound again!

Leave a Reply