search

Toxaris / pts

Interpreter for functional pure type systems.
BSD 3-Clause "New" or "Revised" License
21 stars 7 forks source link

Rethink Term vs. TypedTerm vs. Value #99

Closed Toxaris closed 10 years ago

Toxaris commented 10 years ago

We do lots of strip and reify (inside nbe), so maybe we should shuffle our use of Term, TypedTerm and Value around. Also, we should more clearly state the invariants that come with these representations, and the pre- and postconditions of various functions.

For example, eval takes a Term, but I think one shouldn't call eval on an ill-typed term. So one should always call typecheck* first, getting a TypedTerm and then strip it again in order to eval it. Maybe eval should take a TypedTerm then.

But then there's reify which currently returns Term. Of course, the result of reify should always be well-typed, but currently reify doesn't keep the type annotations, so reify cannot return a TypedTerm.

Blaisorblade commented 10 years ago

But then there's reify which currently returns Term. Of course, the result of reify should always be well-typed, but currently reify doesn't keep the type annotations, so reify cannot return a TypedTerm.

On this matter, we have discussed writing typedNbe: in some situation we currently need some sort of "evaluator" which keeps type annotations, but we currently use typedSubst which is less performant. (But in fact, typedNbe evaluates "too much", which wastes work, though the result is still "correct".

Moreover, it performs unrestricted inlining, so that traversing the result might take exponentially more time. To avoid that, one needs an output normal form which allows for sharing — I've successfully used lets and A-normal form for this reason in my implementation of NbE in inc-lc/ilc-scala.

Blaisorblade commented 10 years ago

Fixed by #106.

Blaisorblade commented 10 years ago

Fixed by #106.

AFAIK, without adding lets to reify, so maybe that's not even needed.

Toxaris commented 10 years ago

About the (still) missing sharing: The key is in this part of PTS.Dynamics.Evaluation:

close :: Name -> Value Eval -> Maybe C -> Value Eval -> Eval (Function Eval)
close name typ sort value = do
  term <- reify value
  abstract (\arg -> do
    withEnvironment [] $ do
      bind name (Binding False arg typ sort) $ do
        eval term)

The potential problem is that term is in normalform, so it might be huge, and then eval term has to traverse this huge term.