JuvixCore

[lukaszcz]

JuvixCore framework and evaluator.

Description

JuvixCore is the Core internal representation for Juvix. It is based on a simple extended lambda-calculus, stripped down enough to enable easy compilation, but high-level enough to enable easy translation from the frontend.

Checklist:

• Node datatype
• Info datatype
• Recursors on Node
• Evaluator
• Typeclass instances for Node:
  • Equality (need to ignore Info)
  • Pretty printing
• Errors
• Parser for Node
• Evaluator CLI
• Evaluator tests
• Strings
• IO monad builtins
• Transformations:
  • Eta-expansion of builtin and constructor applications

[lukaszcz]

Regarding the Bound library, it does not seem fit for our purposes because of complexity issues. We end up with Node traversals (umaps, ufolds) in O(n^2). This is not acceptable, because n may be proportional to the size of the input program. We should try to keep traversals at O(n) or close. This seems to be the problem with most approaches based on "locally naming" free variables. The problem is more clearly visible in the paper http://www.cs.ru.nl/~james/RESEARCH/haskell2004.pdf on which the Bound library is partly based. There, both "abstract" and "instantiate" are clearly linear in the input term. The Bound library seems to mitigate this slightly by not requiring to walk into whatever you're substituting for to change the free variables to avoid capture. But you still need to walk the term you're instantiating to find the variables you need to substitute. Hence, it seems both instantiation and abstraction are still linear.

From https://www.slideshare.net/ekmett/bound-making-de-bruijn-succ-less, succ the whole thing:

"If we could succ an entire expression instead of on each individual variable, we would succ less. Instantiation wouldn't have to walk into that expression at all, and we could lift an Exp into Scope in O(1) instead of O(n)."

This may be confusing, but it seems to refer to what I mentioned above: one can "lift" an entire term we substitute for in O(1) without adjusting its variables to avoid capture. But this doesn't refer to the complexity of instantiation as a whole -- you still need to find the variable you want to instantiate which is linear in the term you substitute into. Reading the source code of Bound seems to confirm this.

In any case, you definitely still need a full tree traversal when walking under binders:

From https://www.slideshare.net/ekmett/bound-making-de-bruijn-succ-less, walking under binders:
nf (Lam b) = Lam $ toScope $ nf $ fromScope b

From Hackage description:
toScope :: Monad f => f (Var b a) -> Scope b f a
Convert from traditional de Bruijn to generalized de Bruijn indices.
This requires a full tree traversal

[lukaszcz]

Regarding Data.TMap, it has very fast lookup because it's based on arrays, but insertion and deletion are O(n) where n is the number of keys. This should be OK for our purposes, because we have only a small constant number of different infos at any given node, and we'll be doing lookup more often than insertion or deletion.

I still think we should change our Info type currently based on HashMaps to TMap, but we should be aware of the O(n) insertion/deletion issue, in case the above assumptions no longer hold in the future.

[lukaszcz]

The typerep-map package (with TMap) requires base < 4.15 and ghc-prim < 0.7. We have base = 4.16 and ghc-prim = 0.8. So I will keep the HashMap-based implementation for now. We can decide what to do with this later.

[paulcadman]

These changes do not affect the rest of the compiler (yet), are very well tested and @lukaszcz explained the main ideas to us in person. I propose we merge this PR now so we can begin work on integration with the rest of the compiler.