« CVS Updates
Durham (11/01/04) »

Term.lhs

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

This entry was posted on Thursday, January 20th, 2005 at 8:49 am and is filed under Hacking. You can follow any responses to this entry through the RSS 2.0 feed. You can skip to the end and leave a response. Pinging is currently not allowed.

4 Responses to “Term.lhs”

  1. Conor Says:
    January 20th, 2005 at 10:06 am

    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:
    January 20th, 2005 at 1:56 pm

    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
    STOP
    B (All,Impl) (R *) (Sc (B (All,Expl) (V 0) (Sc (V 1))))

  3. pwm Says:
    January 20th, 2005 at 2:28 pm

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

  4. Conor Says:
    January 23rd, 2005 at 10:33 pm

    More excitement!


    *TermParser> testTermParser
    (λ X : * ⇒ (λ x : X ⇒ (λ y : X ⇒ *) x)) * : ∀ x : * ⇒ *
    STOP
    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