• Is an Extension of HR with Names

• Short Lived

• De Brujin indices

• Extensions via Extensible

• Idea of terms and values

  • Values have no β-redexs by construction

    • Free name can still be there, and could be inlined

    • Impossible to reduce if the Free names are a data type function

• 

  • In this diagram we can see various mappings that happen through the extensions of core.

• Main representation

Type checking is the first phase of IR. This phase annotates every node with its type and usage. To facilitate fast type checking every type annotated is a fully evaluated value. Other phases like the unifier use this concept as well.

• This is the backend specific form that Michelson uses.

• A lot of the global information predates the frontend context. A lot can probably be integrated.

• Raw Globals Type is a term, which may not be correct (what the user wrote), Regular global the types are values, which can be checked for equality eaiser.

  • Only safe to eval something after it's been type checked

  • Way to unify?

• substWith: Substitutes any term a with an IR.Elim', but results in a term of type a.

• substTermWith: Substitutes any term a with an IR.Elim', and results in an IR.Elim'.

• gsubstWith: Generic substitution of f t with an IR.Elim', and results an f t again. This generic is used for automatic deriving of instances using GHC.Generics.

The functions are for substituting patterns, each of them take:

• A number indicating the current traversal depth.

• A IR.PatternMap containing pairs of pattern variables and terms.

All the functions return an Either with a PatternVar in case not substitution has happened, and the resulting term in case of a substitution.

• patSubst': Substitutes any term a with any of the patterns provided in the map, and results in an a.

• patSubstTerm': Substitutes any term a with any of the patterns provided in the map, and results in an IR.Term'.

• gpatSubst': Generic substitution any term f t with any of the patterns provided in the map, and results in an f t. This generic is used for automatic deriving of instances using GHC.Generics.

This phase simply removes the names from the HR form and constructs a De-Brujin index from the names given in HR.

• The algorithm for this for Terms and Elims is rather simple

  1. When we see a binder (Pi, Lam, Sig, or Let), push the name to the stack for the form in which it is scoped over. Recurse and form and reconstruct said binder.

  2. For forms without names, recurse and reconstruct.

  3. When a name appears, look up it's index from the stack, this is the De-Brujin index we care about. If the Index is not there then we mark it as a Global

HR-Pattern's work in a different way, since patterns are disconnected from terms themselves and do not interact, they work on a system of registering pattern variables, when we come across the binder form =

This conversion adds back names to the IR form. This is mainly used for Pretty Printing.

• The algorithm for Terms and Elims is once again rather simple

  1. When we see a binder (Pi, Lam, Sig, or Let), generate a new name, and push it to the stack. Recurse and form the reconsturct said binder

  2. Forms without names just recurse and reconsturct.

  3. When a name appears, lookup the index from the stack, that position is the name which we care about.

Types used throughout the typechecker (at least I think that's the intent):

• PipelineError

  Includes TypecheckerError, which we currently exit with when a user program is incorrectly typed. (I expect the long-term plan is to produce from it a human-readable error message.)

• PipelineLog

  Used with @"log" (from Capability.Writer) to log a couple of types of events.

• TermAssignment, AssignWithType

  Maps from variables to formulae of Elementary Affine Logic (EAL) / Elementary Affine Core (EAL). These terms are translated to interaction nets, which Juvix uses as its execution model.

  I didn't find any uses of these types that weren't ultimately within the InteractionNetIR module, so they should probably be moved there.

Aliases for types and functions from IR/Typechecker.

• Types

  Aliases for types and functions from IR/Types/Base and IR/Types/Globals, and some simple queries on them. There is one significant pair of mutually recursive functions here: quote :: Value -> Term and neutralQuote :: Neutral -> Elim. (As we shall see below, a Neutral is a particular kind of Value, and may include a Value, hence the mutual recursion.)

• Types/

  • Base

    • The definitions in terms of primitive types of several internal types. For example, a BoundVar is represented by a Natural, and a PatternVar by an Int. Name s are either Global s or Pattern s; the implementation of GlobalName is defined in the NameSymbol library.

    • GlobalUsage is defined here and restricted to only Zero or Omega, but there is a TODO comment asking whether globals might have other usages.

    • Several of the most pervasive data types are defined here, all as extensible, in the sense of trees-that-grow, meaning that different modules can extend them in their own ways, to use their own specific types of annotations, producing versions with a ' suffix:

      • Term Since Juvix is dependently-typed, a type (PrimTy) is one kind of term.

      • Elim An Elim may be a bound variable, a free variable, an application of an Elim (to a Term), or a usage annotation. An Elim is also a term (it may be embedded in a Term with the Elim constructor). Elim is so-called because McBride calls this type an "elimination" in I Got Plenty o' Nuttin'.

        Elim may be viewed as a term that can be inferred (synthesized).

      • Value Since Juvix is dependently-typed, a type (VPrimTy) is one kind of value. Value's definition strongly resembles that of Term, but there are differences; for example, there are let Term s, but no let Value.

      • Neutral Neutral is to Value as Elim is to Term: A Neutral is a bound variable, a free variable, or an application of a Neutral (to a Value); a Neutral is also a Value (it may be embedded in a Value with the VNeutral constructor).

        A Neutral may be viewed as a "stuck term": one for which typechecking must be deferred until some other term(s) has/have been typechecked. (Perhaps this is the source of the name "neutral" – it's neither good (definitely typechecks) nor bad (definitely doesn't typecheck) yet?)

      • Pattern Patterns contain PVar s which are bound by successful pattern matches, as well as primitive values, terms, and pairs and lists of Pattern s.

  • Globals

    • Many Constraint-valued definitions which allow multiple instance s of various classes for various types to be declared at once. (For example, RawGlobalAll allows any type which satisfies it to derive Show, Eq, and Data, among others.)

    • Several more pervasive types, built upon those in Base:

      • Pos, representing strict positivity (or otherwise)

      • FunClause', which defines the form of Juvix function definitions. It comprises arguments (a Telescope), a pattern match (a list of Pattern'), a body, a type, and Bool fields indicating whether the clause is a catchall and/or unreachable.

      • A Function' comprises a NonEmpty list of FunClause' s.

      • The widely-used DataArg' includes a name, a usage, and a type.

      • A Datatype' includes a name, DataArg' s (each with a Pos), a universe level, and a list of constructors (DataCon').

      • A type constructor – DataCon' – includes a name, a type, an the function which defines it (whose output type is the type of the constructor).

      • Raw forms of the above. In each case, the Raw form uses Term where the non-Raw (Cooked?) form uses Value.

• Typechecker

  There's only one definition in this module, but it's a big one: typeCheckDeclaration, which takes a telescope, a list of datatypes, and a list of functions, and calls typeCheckAllCons (see below) on each datatype in the list. If type-checking is successful, it adds the datatype and its constructors to the globals.

  As I write, typeCheckDeclaration is incomplete: it doesn't use one of its parameters, the one comprising a list of function declarations; furthermore, nothing actually calls it yet (except itself, recursively). That is because we simply haven't gotten to writing the typechecking of functions yet (which is also why the backend-specific typecheck functions currently inline everything recursively starting with main).

• Typechecker/

  Some of the types in Typechecker/ are parameterized over back-ends through the Parameterisation type which each back-end exports.

  • Types

    Contains typechecker-specific extensions of some core types:

    • Annotation': Adds usage and type.

    • BindAnnotation': Adds an Annotation' for both the binder and the term that introduces the binder (Lam or Let).

    • Term': Annotations for each of the constructors of Term s (pairs, pi-types, sigma-tyoes, Elim' s, and so on).

    • Elim': Annotations for each of the constructors of Elim s (bound and free variables and applications of them).

  • Env

    The typechecker's extension of EnvCtx is a GlobalsT, which is a (hash)map of names to Global' s, which in turn may be datatypes, data constructors, functions, or Value s (with names and usages). Env therefore also defines a HasGlobals alias for HasReader "globals".

    The interaction with the evaluator, as required by dependent typing, appears in this module via the CanTC type, which requires instances for Eval.HasSubstValue, Eval.HasPatSubstTerm, and Eval.HasWeak.

    This module also defines a Context as a list of the typechecker-specific form of Annotation. There is also a usage context, UContext, which is a list of Usage.

    Pattern bindings and usages – PatBinds and PatUsages – are defined as IntMap s to annotations and usages, respectively, reflecting the use of de Bruijn indices.

    Env also defines the typechecker's State monad: InnerState, which contains a Parameterisation, a PatBinds map, and a Context. (There's a lot of boilerplate related to it.)

    Env also defines signatures: SigDef is a sum of function, constructor, and datatype signatures. Signature maps global names to SigDef s, so it represents all the signatures in global scope. Typechecking functions return Signature s through the TypeCheck type, which uses Capability, with the name "typeSigs".

  • Error

    Defines which errors can occur during typechecking. TypeMismatch, for example, represents a unification error on a variable. Other errors largely follow the possible types of terms – universe mismatches, usage mismatches, non-function types where function types are expected, incompletely-applied data constructors, and unbound variables. Again because dependent typing makes the typechecker depend on the evaluator, the typechecker may also wrap an error from the evaluator (Core/IR/Evaluator/Types.Error).

    The module also provides pretty-printing and an exception wrapper for the main TypecheckError type.

• CheckDatatype

  Exports two interfaces, which between them allow the type-checking of datatype declarations; hence, both are called by typeCheckDeclaration :

  • checkDataType

    Typechecks all the parameters of a datatype declaration, ultimately by calling typeTerm on each.

  • typeCheckAllCons

    Typechecks all the constructors of a datatype declaration, ultimately by calling typeTerm on each, followed by evalTerm, because of the potential dependency of types on values.

• CheckTerm

  Exports typeTerm, through which the typechecker is plugged into the Pipeline, via typecheckEval and typecheckErase, and through them from coreToAnn, which is called from the backend-specific typecheck functions with the appropriate Parameterisation s. (The backend-specific typecheck functions in the current development branch, as I write, have a lot in common, but Alberto is factoring them out as part of PR 821.)

  Internally, typeTerm is implemented in terms of the mutually-recursive typeTerm' and typeElim' (which follow the structures of the mutually-recursive Term and Elim). These two functions are, in a sense, the core of the typechecker: they're the expression in code of the typing rules of QTT. For example, when typeTerm' is given a lambda with expected type A -> B, it checks whether assuming that the variable has type A results in the body correctly typechecking (with a recursive call to typeTerm') with type B.

  The mutual recursion expresses the bidirectionality of the type checking: annotated terms are checked by typeTerm' ; unannotated terms ("eliminations") have their types inferred (synthesized) by typeElim'.

  (Note: as of this writing, there is a bug in the Pair' case of typeTerm' : it doesn't evaluate the left term in checking the type of the right, so it wouldn't handle dependent pairs correctly. I will fix that shortly.)

  One of the types that appears as a frequent return value in CheckTerm.hs is Leftovers. This type keeps track of variables which haven't yet been used as often as their Usage annotation allows – and, if it's not omega, requires! Hence if there are any Leftovers with usages other than omega after a term has been type-checked, that causes a LeftoverUsage TypecheckerError to be thrown.

  CheckTerm.hs is also the location of our definition of the subtyping relation, operator <:.

  Many of the return values of functions in CheckTerm.hs are parameterised over Monad s with constraints such as HasThrowTC' and HasBound. So they expect to be able to throw TypecheckerError s, or to be called as part of the execution of a state monad containing (at least) a list of bindings. That's a pattern which strikes me as crying out for algebraic effects – I think they could make the signatures much more readable, with less boilerplate and less code to compose effects. So I feel this module should be able to "read" better when it's written in Juvix itself!

• TransformExt

  This module defines an interface for transforming one extension of a Term (in the sense of trees-that-grow) into another extension of Term – an applicative functor on term extensions. Such functors are defined in terms of their operations on each variant of Term, such as primitive, pi-type, let-binding, and so on. Such functors compose (and the TransformExt module define the compose function which composes them). This module also defines a forgetful functor, forgetter, which transforms an extended Term into a Term with no extension (NoExt).

  There are forgetful uses in the Evaulator and Erasure modules, but I haven't found any non-forgetful uses yet.

• TransformExt/

  • OnlyExts

    OnlyExts is so-called because it defines a Term -transforming functor which discards annotations but preserves extensions.

• Types

  The typechecker-specific annotation of terms comprises:

  • A usage (any natural number, or omega)

  • A term of QTT (which might be a type), which is one of:

    • * (a universe, of which there is a natural-number-indexed hierarchy)

    • a primitive type

    • a primitive constant

    • a pi-type (dependent product)

    • a lambda

    • a sigma type (dependent sum)

    • a pair

    • a let-binding

    • the unit type

    • the unit value

    • one of the Elim types:

      • a bound variable

      • a free variable

      • an application of an Elim to a Term

      • a Term annotated with a Usage

    Some of these terms are extensions to core QTT, which, for example, does not appear to me to define explicit pair types, for example.

• Erasure

  This module just defines two forgetful functors, for Term and Elim, which discard extensions (see TransformExt).

Every important operation in this phase is a direct Syntax to Syntax transformation with no extra context needed.

The function op pipes all desugaring functions that do not require a context.

  -- | @op@ fully desugars the frontend syntax from the original
  -- frontend s-exp representation to a form without modules, conditions,
  -- guards, etc. This pass thus does all transformations that do not
  -- requires a context
  op :: [Sexp.T] -> [Sexp.T]
  op syn =
    syn
      >>| Pass.moduleTransform
      >>| Pass.moduleLetTransform
      >>| Pass.condTransform
      >>| Pass.ifTransform
      >>| Pass.multipleTransLet
      |> Pass.multipleTransDefun
      |> Pass.combineSig
      >>| Pass.removePunnedRecords
      >>| Pass.translateDo

The order of these passes is relatively arbitrary. We simply remove modules, then module lets, then conds, then …, and then do. The op function is ran directly on the output of the last phase.

Examples of its use are provided in the EasyPipeline module (run desugar1 and desugar2 to test the results for yourself!).

  ;; From Design/S-expression Syntax
  (:defun foo (x)
    (:cond
      ((:infix == x 2) (:infix + 3 (:infix + 4 x)))
      (else            (:infix + x 2))))

  -- | @Defun@ is the base defun structure
  -- currently it does not have matching
  data Defun = Defun
    { defunName :: Sexp.T,
      defunArgs :: Sexp.T,
      defunBody :: Sexp.T
    }
    deriving (Show)

  ----------------------------------------
  -- Defun
  ----------------------------------------

  nameDefun :: NameSymbol.T
  nameDefun = ":defun"

  isDefun :: Sexp.T -> Bool
  isDefun (Sexp.Cons form _) = Sexp.isAtomNamed form nameDefun
  isDefun _ = False

  toDefun :: Sexp.T -> Maybe Defun
  toDefun form
    | isDefun form =
      case form of
        _Defun Sexp.:> sexp1 Sexp.:> sexp2 Sexp.:> sexp3 Sexp.:> Sexp.Nil ->
          Defun sexp1 sexp2 sexp3 |> Just
        _ ->
          Nothing
    | otherwise =
      Nothing

  fromDefun :: Defun -> Sexp.T
  fromDefun (Defun sexp1 sexp2 sexp3) =
    Sexp.list [Sexp.atom nameDefun, sexp1, sexp2, sexp3]

  λ> Right defun = Sexp.parse "(:defun foo (x) (:cond ((:infix == x 2) (:infix + 3 (:infix + 4 x))) (else (:infix + x 2))))"
  λ> import qualified Juvix.Sexp.Structure as Structure
  λ> Structure.toDefun defun
  Just (Defun {defunName = "foo", defunArgs = ("x"), defunBody = (":cond" ((":infix" "==" "x" 2) (":infix" "+" 3 (":infix" "+" 4 "x"))) ("else" (":infix" "+" "x" 2)))})

  ;; 1
  (generate-haskell "Defun" '("sexp" "sexp" "sexp") ":defun")

  ;; 2
  (generate-haskell "ArgBody" '("sexp" "sexp") nil)

  ;; 3
  (generate-haskell "DeconBody" (repeat 2 "sexp") nil)

  (generate-haskell "Case" '("sexp" "deconBody") "case" :list-star t)


  ;; 4
  (generate-haskell "NotPunned" '("sexp" "sexp") nil)

  (generate-haskell "RecordNoPunned" '("notPunnedGroup") ":record-no-pun"
                    :list-star t
                    :un-grouped t)

  ;; 5
  (generate-haskell "ArgBody" '("sexp" "sexp") nil)
  ;; bodys here, as there are multiple!
  (generate-haskell "LetMatch" '("sexp" "argBodys" "sexp") ":let-match")

  -- | @PredAns@ is an abstraction over questions and answers
  data PredAns = PredAns {predAnsPredicate :: Sexp.T, predAnsAnswer :: Sexp.T}
    deriving (Show)

  -- | @Cond@ here Cond form takes a list of predicate answers
  newtype Cond = Cond {condEntailments :: [PredAns]} deriving (Show)

  (generate-haskell "PredAns" (repeat 2 "sexp") nil)

  (generate-haskell "Cond" '("predAns") ":cond" :list-star t)

  λ> Right cond = Sexp.parse "(:cond ((:infix == x 2) (:infix + 3 (:infix + 4 x))) (else (:infix + x 2)))"
  λ> Structure.toCond cond
  Just
    (Cond
       {condEntailments =
          [PredAns { predAnsPredicate = (":infix" "==" "x" 2)
                   , predAnsAnswer = (":infix" "+" 3 (":infix" "+" 4 "x"))}
          ,PredAns { predAnsPredicate = "else"
                   , predAnsAnswer = (":infix" "+" "x" 2)}]})

  -- | @If@ has an pred, then, and else.
  data If = If
    { ifPredicate :: Sexp.T,
      ifConclusion :: Sexp.T,
      ifAlternative :: Sexp.T
    }
    deriving (Show)

  -- | @IfNoElse@ has a pred and a then.
  data IfNoElse = IfNoElse
    { ifNoElsePredicate :: Sexp.T,
      ifNoElseConclusion :: Sexp.T
    }
    deriving (Show)


  -- In the generator
  (generate-haskell "If" (repeat 3 "sexp") "if")
  (generate-haskell "IfNoElse" (repeat 2 "sexp") "if")

  condToIf condExpression
      | Just cond <- Structure.toCond condExpression,
        -- we need to setup the if with no else
        Just last <- lastMay (cond ^. entailments) =
        let acc =
              -- let's create it, with the predicate and answer of the
              -- PredAns tye
              Structure.IfNoElse (last ^. predicate) (last ^. answer)
                |> Structure.fromIfNoElse
         -- Now let us employ the fold strategy we talked about
         in foldr generation acc (initSafe (cond ^. entailments))
      | otherwise = error "malformed cond"
    where
      -- this is the folded function, see how we just build up the if,
      -- then push it back to an s-expression at the end?
      generation predAns acc =
        Structure.If (predAns ^. predicate) (predAns ^. answer) acc
          |> Structure.fromIf

  import qualified Juvix.Sexp.Structure as Structure
  import Juvix.Sexp.Structure.Lens
  import Control.Lens hiding ((|>))

  λ> Right cond = Sexp.parse "(:cond ((:infix == x 2) (:infix + 3 (:infix + 4 x))) (else (:infix + x 2)))"

  λ> condToIf cond
  ("if" (":infix" "==" "x" 2) (":infix" "+" 3 (":infix" "+" 4 "x")) ("if" "else" (":infix" "+" "x" 2)))

  -- | @condTransform@ - CondTransform turns the cond form of the fronted
  -- language into a series of ifs
  -- - BNF input form:
  --   + (:Cond (pred-1 result-1) … (pred-n result-n))
  -- - BNF output form:
  --   + (if pred-1 result-1 (if pred-2 result-2 (… (if pred-n result-n))))
  condTransform :: Sexp.T -> Sexp.T
  condTransform xs = Sexp.foldPred xs (== Structure.nameCond) condToIf
    where
      condToIf atom cdr
        | Just cond <- Structure.toCond (Sexp.Atom atom Sexp.:> cdr),
          Just last <- lastMay (cond ^. entailments) =
          let acc =
                Structure.IfNoElse (last ^. predicate) (last ^. answer)
                  |> Structure.fromIfNoElse
           in foldr generation acc (initSafe (cond ^. entailments))
                |> Sexp.addMetaToCar atom
        | otherwise = error "malformed cond"
      --
      generation predAns acc =
        Structure.If (predAns ^. predicate) (predAns ^. answer) acc
          |> Structure.fromIf

  λ> Pass.condTransform cond

  λ> Right cond = Sexp.parse "(:defun f (x) (:cond ((:infix == x 2) (:infix + 3 (:infix + 4 x))) (else (:infix + x 2))))"
  λ> cond
  (":defun" "f" ("x")
     (":cond" ((":infix" "==" "x" 2) (":infix" "+" 3 (":infix" "+" 4 "x")))
              ("else"                (":infix" "+" "x" 2))))
  λ> Pass.condTransform cond
  (":defun" "f" ("x")
     ("if" (":infix" "==" "x" 2)
           (":infix" "+" 3 (":infix" "+" 4 "x"))
           ("if" "else"
                 (":infix" "+" "x" 2))))

The context phase is an important phase, this is where we start to introduce the context and our operations start to revolve around it. This is also where our pipeline starts to show some inadequacies with how we ingest data. But first we must talk about how we transform our list of S-expressions into a context

the parser combinator file that we will be inspecting will be found here.

In order to be able to understand this code, I suggest reading about how parser combinators work, for a very brief rundown here are the key features we will be abusing. If you wish to skip the brief rundown skip to the Specific Information Section.

  matchL :: Parser Types.MatchL
  matchL = do
    skipLiner J.pipe
    match <- P.try matchLogicSN
    spaceLiner (P.string "->")
    Types.MatchL match <$> P.try expression

  topLevel :: Parser Types.TopLevel
  topLevel =
    P.try (Types.Type <$> typeP)
      <|> P.try fun
      <|> P.try modT
      <|> P.try (Types.ModueOpen <$> moduleOpen)

  expressionGen :: Parser Types.Expression -> Parser Types.Expression
  expressionGen p =
    Expr.makeExprParser (spaceLiner (expressionGen' p)) tableExp

  -- For Expressions
  tableExp :: [[Expr.Operator Parser Types.Expression]]
  tableExp =
    [ [refine],
      [infixOp],
      [arrowExp]
    ]

  infixOp :: Expr.Operator Parser Types.Expression
  infixOp =
    Expr.InfixR
      ( P.try $ do
          inf <- spaceLiner infixSymbolDot
          pure
            (\l r -> Types.Infix (Types.Inf l inf r))
      )

  do''' :: Parser Types.Expression
  do''' = Types.Do <$> do'

  app'' :: Parser Types.Expression
  app'' = Types.Application <$> P.try application

  all'' :: Parser Types.Expression
  all'' = P.try do''' <|> app''

  -- used to remove do from parsing
  expression' :: Parser Types.Expression
  expression' = expressionGen app''

  -- used to remove both from parsing
  expression''' :: Parser Types.Expression
  expression''' = expressionGen (fail "")

  expression :: Parser Types.Expression
  expression = expressionGen all''

The transformation file can be found here.

Here we do a very straightforward algorithm, of when we see a particular Juvix ML ADT form, we then transform it to the equivalent Lisp expression that can be found in the s-expression document in design

Ideally we could generate the particulars of the syntax via some schema and have the ML code use that. This would remove the hardbaked structure of each form from the transformation, however with how many different types exist in the frontend form this would be quite a challenge. We do this technique later on in the compiler, reducing the amount of hard baked forms.

The above issue also extrapolates a bit on why we have chosen this path. ML structured ADT's are wonderful, however they lack flexibility. We used a trees that grow structure in the past, however this would convert one rigid ADT into another. And so we had to convert the massive adt that we built one by one, which ended up with over 500 lines of code per pass! However an issue just as big is that no common interface can be had, thus our passes couldn't as easily be abstracted awway.

Sometimes we wish to quantify over symbols which we may add or create. For our previous example, what if Foo.Bar.zed is undefined? Operations which operate over hypothetical symbols have a way to know if the symbol is defined or not.

The resolution rules are fairly simple, but we will investigate them with three case studies where the symbols may be undefined. zed, Foo.zed, TopLevel.Foo.zed

1. zed

   • Since zed is not in scope, we only really have two choices. We either mean Toplevel.zed or CurrentNameSpace.zed. Since we find that we typically mean zed in the current module, and not some hypothetical one at a top level, we try to do the latter. So the operation deals with an undefined CurrentNameSpace.zed

2. Foo.zed

   • Since This case can have a condition where Foo could also be resolved, we break this into another case analysis.

     1. Foo is resolved

        • In this case, we act much like the 1) case, where we explicitly work in an unresolved CurrentNameSpace.Foo.zed. or a Toplevel.Foo.zed depending on which one is in scope (see the scoping section above!).

     2. Foo is not resolved

        • In this case we actually do a different resolution than the zed case. We assume we are talking a toplevel version, namely Toplevel.Foo.zed

3. Toplevel.Foo.zed

   • This one is rather easy as well, as it falls back to case 2 subsection 2.

Overall some of these rules are arbitrary, namely case 2 subsection 2 may need to conform to be more like case 1, however this requires testing and playing with the system more to determine.

Both this section and the above are implemented in the modify speace impure section.

These operations aren't derived from the primitive operations, however are quite important for operation of the context. Some even have special rules one must pay attention to.

  switchNameSpace ::
    NameSymbol.T -> T term ty sumRep -> IO (Either PathError (T term ty sumRep))

This layer of core stand for Human Readable, as we have variable names instead of hairy de-bruijn indices. This phase is shortly lived, as most processing at this level wants to work on some extension of the Internal Representation as names create issues for the various algorithms.

This is where the main process of type checking happens.

• Names are reduced to de-bruijn indices.

• We have many extensions with metadata that fluctuate depending on what pass of core is run.

In this phase of Core, we remove the types from the terms, as they don't serve any computation purpose. By this point we've done most of the processing we need.

In the future I suspect inlining algorithms will either be done here or in IR right above.

• BNF

    input-expresson ::=
        let <let-path-input>+ in <expression>
      | ...
  
    output-expression ::=
        let <let-name-output>+ in <expression>
      | ...
  
    let-pat-input   ::= <name> <pattern>* <guard>+
    let-name-output ::= <name> <name>* <guard>+
  
    guard? ::= \| <expression> = <expression>
             | <expression>

• Examples

    (** Example 1 *)
  
    (* Input *)
    def example =
      let
        foo (Just x) = 5
        foo Nothing  = 6
      in foo (Just ())
  
    (* Output *)
  
  
    (* generated by the pass *)
    def #g:unique-name (Just x) = 5
        #g:unique-name Nothing  = 6
  
    def example =
      #g:unique-name (Just ())
  
  
    (** Example 2 *)
  
    (* Input *)
    def example =
      let foo x = 5 + x in
      foo 3
  
    (* Output *)
    def example =
      let foo x = 5 + x in
      foo 3
  
    (** Example 3 *)
  
    (* Input *)
    def example =
      let foo {x, y} = y + x in
      foo {x = 3, x = 5}
  
  
  
    (* Output *)
    (* generated by the pass *)
    def #g:unique-name {x, y} = x + y
  
    def example =
      let foo x = 5 + x in
      #g:unique-name {x = 3, x = 5}

• Description

  The Transformation takes any let expression with <patterns>*'s that are any form of pattern matching, into top level declarations that are uniquely named for use where the previous let expression was used.

  If the let form has only simple patterns, then we leave it un-transformed, this can be seen in Example 2 in the above code.

• Possible Complications

  • We have to lambda lift extra items which may not be related to this transform see this example

      (* Input *)
      def example =
        let
          def bar x = x
          def foo (Just x) = bar 5
              foo Nothing  = bar 6
        foo (bar (Just ()))
    
    
      (* Output *)
    
      def #g:unique-bar x = x
    
      def #g:unique-foo (Just x) = #g:unique-bar 5
          #g:unique-foo Nothing  = #g:unique-bar 6
    
      def example = #g:unique-foo (#g:unique-bar (Just ()))

• Literature

  See Lambda Lifting

• NOTE, Multiple lets of the same function, not nested

• BNF

    ;; Input
    input-expression ::=
        let <let-name-output>+ in <expression>
      | ...
  
    input-declaration ::=
        def <def-pattern-input>+
      | ...
  
    ;; Ouptut
    ouptut-expression ::=
        let <name> <name>* = <expression> in <expression>
      | ...
  
    ouptut-declaration ::=
        def <def-pattern-ouptut>+
      | ...
  
    ;; Helpers
    def-pattern-input ::= <name> <pattern>* <guard?>
  
    def-pattern-ouptut ::= <name> <pattern>* <expression>
  
    let-name-input ::= <name> <name>* <guard?>
  
    guard? ::= \| <expression> = <expression>
             | <expression>

• Examples

    (** Example 1 *)
  
    (* Input *)
    def add-3 x =
      let bar y = 3 + y in
      bar x
  
    (* Output *)
    def add-3 x =
      let bar y = 3 + y in
      bar x
  
    (** Example 2 *)
  
    (* Input *)
    def add-3-not-on-0 x =
      let compute y
           | y == 0 = Nothing
           | else   = Just (y + 3)
      in compute x
  
    (* Output *)
    def add-3-not-on-0 x =
      let compute y = if (Just (y + 3)) Nothing (y == 0)
      in compute x
  
    (** Example 3 *)
  
    (* Input *)
    def add-3-not-on-0 x =
      let compute y
           | y == 0 = Nothing
          compute y = Just (y + 3)
      in compute x
  
    (* Output *)
    def add-3-not-on-0 x =
      let compute y = if (Just (y + 3)) Nothing (y == 0)
      in compute x
  
  
    (** Example 4 *)
  
    (* Input *)
    def add-3-unless-1-or-0 x
      | x == 0 = 0
      | x == 1 = 1
      | else   = x + 3
  
    (* Output *)
    def add3-unless-1-or-0 x =
      if 0
         (if 1
             (x + 3)
             (x == 1))
         (x == 0)
  
    (* If is defined as follows *)
    (* about usages, consult the following table about
       what we can do usage wise
       cond
         first-class-usages? = if' (* comedy *)
         weakening?          = 1
         else                = ω *)
    sig if : {P : ((x : Bool) -0-> *))}
          -0-> t : P True
          -ω-> f : P False
          -ω-> b : Bool
          -1-> P b
    let if {Proof} then-case else-case True  = then-case
        if {Proof} then-case else-case False = else-case

• Description

  Here we do the majority of the work of removing guards from lets. We can notice that lets and defs can both at this point desugar their guard checks into dispatching to this if destructor function given.

  We can also notice that after we run this, there can be no more lets with multiple patterns as both guards and matches have been handled now.

• Possible Complications

  • We already handle guards in the desugar passes. Currently it just sees the guards as Cond's and desugars them into cases. This is however incorrect as pattern matching has a fall through behavior this does not respect.

    • This can be solved with a proper pattern matching algorithm

  • This algorithm may be better served by the linearization algorithm given by the pattern match simplification. I'm not sure this is always possible in the def case. For the simple lets we currently have this works as a strategy however.

  • This could maybe also be served better with an with pattern through some strategy. See the following.

    
      (* Input *)
      sig foo : maybe (maybe int) -1-> int
      def foo (Just (Just x)) | x == 0      = 3
          foo (Just x)        | x == Just 3 = 5
          foo _                             = 0
    
      (* output *)
      sig foo-inner : maybe (maybe int) -1-> bool -1-> bool -1-> int
      def foo-inner (Just (Just x)) true _    = 3
          foo-inner (Just x)        _    true = 5
          foo-inner _               _    _    = 0
    
      sig foo : maybe (maybe int) -1-> int
      def foo m@(Just (Just x)) = foo-inner m (x == 0) false
          foo m@(Just x)        = foo-inner m false    (x == Just 3)
          foo m                 = foo-inner m false    false

• BNF

    input-expression ::=
        let <name> <name>* = <expression> in <expression>
      | ...
  
    output-expression ::=
        let <name> = <expression> in <expression>
      | ...

• Examples

    (** Example 1 *)
  
    (* Input *)
    def foo =
      let bar a b c = a + b + c in
      bar 1 2 3
  
    (* Output *)
    def foo =
      let bar = λ a ⟶ (λ b ⟶ (λ c ⟶ a + b + c)) in
      bar 1 2 3

• Description

  Here we just take the given let form and transform it into it's pure lambda form for the body.

• Possible Complications

  • The type may need to be explicitly given, thus forcing us to give a signature with our bar.

• BNF

    input-expression ::= open <expression> in <expression>
                       | ...
  
    output-expression ::= open <name> in <expression>
                        | ...

• Examples

    (** Example 1 *)
  
    (* Input *)
    def foo =
      open bar in
      x + y
  
    (* Output *)
    def foo =
      open bar in
      x + y
  
    (** Example 2 *)
  
    (* Input *)
    def foo xs =
      open (fold building-up-a-module xs : mod {…}) in
      x + y
  
    (* Output *)
    def foo xs =
      let sig #:gensym 1 : mod {…}
          def #:gensym = fold building-up-a-module xs
      open #:gensym in
      x + y

• Description

  Here we want to have any non trivial open converted into a form where we let a name bind to this complicated expression and then have that name be used once in the open expression.

• Possible Complications

  • There is an outstanding question of how opens relate to de-buijn indicies.

    • Maybe name resolution can help sort this out?

  • Type resolution of the module is also an interesting question to answer as well.

• Literature

• BNF

    term-input ::= λ <name> ⟶ <expression>
                 | let <usage> <name> ...
                 | sig <usage> <name> ...
                 | pi  <usage> <name> ...
                 | ...
  
    term-output = λ ⟶ <expression>
                 | let <usage> = <expression>
                 | sig <usage> ...
                 | pi  <usage> ...

• Examples

    (** Example 1 *)
  
    (* Input *)
    def foo a b =
      let add-them = a + b in
      λ d ⟶ d + add-them
  
    (* Output *)
    def foo (Global-Pat 0) (Global-pat 1) =
      let (global-pat 0 + global-pat 1) in
      λ ⟶ indicy 0 + indicy 1
  
    (** Example 2 *)
  
    (* Input *)
    def foo (Just a) (List b c d) =
      let add-them = a + b in
      λ d : (Π 0 (x : Nat.t) Nat.t)  ⟶ d + add-them + c + d
  
    (* Output *)
    def foo (Just (Global-pat 0))
            (List (Global-pat 1) (Global-pat 2) (Global-pat 3)) =
      let (global-pat 0 + global-pat 1) in
      λ : (Π 1 Nat.t Nat.t)  ⟶ indicy 0 + indicy 1 + global-pat 2 + global-pat 3
  
    (** Example 3 *)
  
    (* Input *)
    def foo (Just a) (List b c d) =
      let add-them = a + b in
      λ typ : (Π 0 (typ : ×₀) (Π 1 typ typ))  ⟶
        λ d ⟶
          d + add-them + c + d
  
    (* Output *)
    def foo (Just (Global-pat 0))
            (List (Global-pat 1) (Global-pat 2) (Global-pat 3)) =
      let (global-pat 0 + global-pat 1) in
      λ : (Π 0 ×₀ (Π 1 (indicy 0) (indicy 1))) ⟶
       λ ⟶
         indicy 0 + indicy 2 + global-pat 2 + global-pat 3

• Literature

  See De Bruijn

• Description

  Here we simply run a simple De Bruijn algorithm. In our code base this is actually already fully implemented

• Possible Complications

  • Bug see issue #864, namely we are inconsistent about how we handle recursive lets

    • Local recursive functions have to be lambda lifted per discussion

  • How do we treat opens in terms of de-bruijn indicies?

• BNF

    input-expression ::= open <name> in <input-expression>
                       | ...
    ;; remove open
    ;; Note that in more complex cases this may not be possible, so we may
    ;; not have any bnf changes in this pass
    output-expression ::= ...

• Examples

    (** Example 1 *)
  
    (* Input 1 *)
  
    (* Written by the user, which is part of the env by now *)
    open Prelude
  
    (* Input we see at this level *)
    sig add-list : Int.t -> List.t Int.t -> Int.t
    def
      add-list (global-pat 0) (Cons (global-pat 1) (global-pat 2)) =
        open Michelson in
        (* + is in Michelson *)
        let global-pat 0 + global-pat 1 in
        add-list (indicy 0) (global-pat 2)
      add-list (global-pat 0) Nil =
        global-pat 0
  
    (* Output *)
    sig add-list :
      Prelude.Int.t Prelude.-> Prelude.List.t Prelude.Int.t Prelude.-> Prelude.Int.t
    def
      add-list (global-pat 0) (Prelude.Cons (global-pat 1) (global-pat 2)) =
        open Prelude.Michelson in
        (* + is in Michelson *)
        let global-pat 0 Prelude.Michelson.+ global-pat 1 in
        add-list (indicy 0) (global-pat 2)
      add-list (global-pat 0) Prelude.Nil =
        global-pat 0

• Description

  Here we run name resolution, for top level opens, this is rather simple, as our current Contextify step notes top level opens. Thus what needs to be respected is how opens effect the closure and determine for that what is referencing to outer names.

• Possible Complications

  • To get complex opens working, we need to do some form of type checking. Thus this might have to be integrated to some level of type checking.

• Literature

• BNF

    input-expression ::= <input-expression> <op> <input-expression>
                       | ...
  
    output-expression ::= ...

• Examples

    (** Example 1 *)
  
    (* Input *)
    (* * has precedence left 6  *)
    (* + has precedence 5  *)
    def foo = a * b * d + c
  
    (* Output *)
    def foo = + (* a (* b d))
                c

• Description

  Here we have to resolve infix symbols into prefix symbols given some precedence table. The easiest way to do this is to modify the Shunt Yard algorithm slightly for the constraints of Juvix. Thankfully this is already in.

• Possible Complications

  • One has to be careful about how infixl, infixr and infix all interact with each other.

• Literature

  See Shunt Yard

• BNF

• Examples

• Description

• Possible Complications

• Literature

• BNF

    ;; No BNF changes

• Examples

    (** Example 1 *)
    (* Example may be artificial *)
    (* Input *)
    sig linear-comb-pos-nats
      : Π 1 Nat.t
           (Π 1 Nat.t
                (Π 2 Nat.t
                     (Π 0 (>= (indicy 0) 1)
                          (Π 0 (>= (indicy 2) 2)
                               (refinement Nat.t (> (indicy 0) 1))))))
    (* global-pat 3 and global-pat 4 are the 0 usage proofs *)
    def pos-linear-comb (global-pat 0)
                        (global-pat 1)
                        (global-pat 2)
                        (global-pat 3)
                        (global-pat 4) =
      let ( * (global-pat 2) (global-pat 1)) : 1 Nat.t in
      (* Let's prove that our result is at least (max (arg 1) (arg 2)),
         using our proofs of (arg 3) and (arg 4) *)
      let times-by-ℕ⁺-is-greater (indicy 0) (global-pat 3) (global-pat 4) : 0 Nat.t in
      refinement (+ (indicy 1) ( * (global-pat 0) (global-pat 3))) (indicy 0)
    (* Output *)
  
    sig linear-comb-pos-nats
      : Π 1 Nat.t
           (Π 1 Nat.t
                (Π 2 Nat.t
                     (Π 0 (>= (indicy 0) 1)
                          (Π 0 (>= (indicy 2) 2)
                               (Refinement Nat.t (> (indicy 0) 1))))))
    (* global-pat 3 and global-pat 4 are the 0 usage proofs *)
    def pos-linear-comb (global-pat 0)
                        (global-pat 1)
                        (global-pat 2)
                        (global-pat 3)
                        (global-pat 4) =
      let ( * (global-pat 2) (global-pat 1)) : 1 Nat.t in
      (+ (indicy 0) ( * (global-pat 0) (global-pat 2)))

• Description

  In this code we want to remove any code which has 0 usages in them. In particular, we can see in Example 1 that the proof about the number being greater than 1 is fully erased.

  However, it is important to note a few points. We did not erase the passing of extra arguments to linear-comb-pos-nats. This is because these arguments are still passed on the application side, both in existing code and in any incremental compilation passes. These arguments are ignored. Alternatively, we could chose a strategy such that it's noted what the 0 usage arguments are, but have a shim layer that transforms arguments before application with functions with 0 argument functions.

• Possible Complications

  • What to do with 0 usage function arguments. See Description for another method of doing this.

  • What do we do about top level records usage wise? We need the 0 usage arguments, so we have to treat them in an interesting way.

  • We need to preserve signatures which only partially care about usage erasure.

• Literature

• BNF

• Examples

• Description

• Possible Complications

• Literature

• BNF

• Examples

• Description

• Possible Complications

• Literature

• BNF

• Examples

• Description

• Possible Complications

• Literature

• BNF

• Examples

• Description

• Possible Complications

• Literature

• BNF

• Examples

• Description

• Possible Complications

• Literature

Need eval? How does this reflect in the pipeline

We want to structure the typeCheckEvalLoop as follows

  throw CantResolveSymbol ~> nameResolution

  -- typeChecking does
  -- Hole insertion, unifier, Type Checking, nameResolution
  typeCheckEvalLoop =
    doesAthing
      {resolverEffects
          = {
            -- filling holes
            , UnifyImplicits    ~> unifier
            -- Creating holes for the unifier to fill
            , InsertImplicit    ~> implicitInsertion
            -- For evaling terms
            , Evaluate          ~> eval
            -- For first class Name Resolution
            , CantResolveSymbol ~> nameResolution
            }}

def bar =
  let
    mod baz =
      mod biz =
        def foo = 3.
  baz.biz.foo
   ~> 0.biz.foo
   ~> resolve-symbol (resolve-symbol foo biz) 0

def bar =
  let mod bar =
      def foo = 3.
  let #g:gensym = (bar djfka djfkas dfjak)
  open #g:gensym ~> open with type {foo}
  resolve-symbol foo #g:gensym.

def bar =
  let mod bar x y z =
        def foo = 3.
  let #g:gensym = (bar djfka djfkas dfjak)
  open #g:gensym ~> open with type {foo}
  resolve-symbol foo #g:gensym.


def bar =
  let mod bar x y z =
        def foo = 3.
  open (fold function-generating-a-module xs : mod {…})
  resolve-symbol foo #g:gensym.

def bar =
  let mod bar x y z =
        def foo = 3.
  let def #g:gensym =
        fold function-generating-a-module xs : mod {…}
  open-simple #g:gensym
  resolve-symbol foo #g:gensym.

1. Inlining

1. Making a fast curry

1. Lambda-Lifting in Quadratic Time*

1. Benjamin C. Pierce: Types and Programming Languages chapter 6 page 75-80

1. Shunt Yard Algorithm

An instance of HasBackend, that implements the main connection to the pipeline:

• The datatype used for types, values and errors (Ty, Val, Err

respectively);

• stdlib, the Juvix source file(s) that make up the standard library for

this backend;

• Optionally an implementation for the parse function;

• Optionally an implementation for the typecheck function;

• An implementation for the compile function.

We need to inform the Juvix compiler of some basic information about our backend, such as:

• A function for typechecking primitives: hasType.

• Lists of builtin values and types: builtinTypes and builtinValues.

• Functions for creating primitives based on a literal integers, floats or strings: stringVal, intVal and floatVal.

For compilation, the backend takes a representation of the input program that is very close to a primitive-extended lambda calculus with multi-argument lambda's. As the primitives of the target language themselves can be functions, for example basic arithmetic operators, we can normalize these terms as well. For this we need to instantiate two classes for the primitives:

• HasSubstV: For substitution of term.

• HasWeak: For weakening of terms (accounting for removal of a lambda abstraction).

• HasPatSubstTerm: Substitution of patterns.

Each of these are documented in more detail at the evaluator page.

Additionally, to make applying terms possible during substitution, the CanApply class needs to be instantiated for primitive terms and types.

The LLVM backend uses an intermediate representation for primitives that are specific to LLVM: RawPrimVal for values and functions, and PrimTy for types. Each of these have a rather direct relation to constructs available in LLVM.

It is possible that primitives are terms that can be reduced further, i.e. addition of two constants can be replaced by a single constant. To support this, the LLVM backend implements application of terms by instancing the CanApply class for both types and values.

The parameterisation of the LLVM backend is really easy and follows implementation of the Parameterisation datatype:

• hasType is a function that checks the types for raw primitive values. Currently the typechecking is very basic, it just checks if the given types matches with the primitive value in arity. For operator primitives, we check if the types of the arguments are equal. This implementation will definitely have to be refined in the future.

• builtinTypes and builtinValues just provide a mapping from source code literal names to the actual literals.

• integerToRawPrimVal creates a literal based on an integer. Currently it doesn't take the size of the literal into account, as integer literals always share the same type. This should be improved in the future.

• There are currently no implementations for stringVal and floatVal, as the backend does not support these types yet.

For simplicity, the current HasWeak, HasSubstValue and HasSubstTerm instances do not do anything at all. This will likely change in the future.

The LLVM instances for HasBackend relies on the default for the parse function. Additionally:

• The typecheck function relies on the general typechecker implementation by calling the typecheck' function, together with the parameterisation and a the LLVM representation of a set type.

• The compile function, which gets a filename and an annotated term (AnnTermT) as the program. The annotated term with typed primitives is translated to an annotated term with raw primitives RawPrimVal. These are then translated to LLVM code.

With the input program being represented by the annotated Term, we can now easily translate these to LLVM code. We rely mostly on the llvm-hs-pure package, as it provides a nice monadic interface LLVM.IRBuilder that keeps track of variables for us. Therefore, the implementation is rather straightforward:

• The whole program, is translated to an LLVM module by the compileProgram function. This module contains a hardcoded main function, with the type taken from the outermost annotated term.

• The term itself is compiled by the compileTerm function, using recursion for any sub terms.

• For any primitive functions, we check if enough arguments are available, and if so the primitive function is written, with unnamed references to the arguments all taken care of by the IRBuilder monad.

Each of these functions are called in their own part of the pipeline, the output of parse is the input of typecheck and the output of typecheck is the input of compile.