• Growing a language

  • A wonderful talk by guy Steele on why a language should allow user's features to feel built in.

First class environments are a way of making the environment code lives in first class. This means we could talk about discrete environments and more easily distinguish between startup, compilation time, evaluation time, etc environments. There are many bigger implications as well, like being able to talk about environments over the network, having sandboxed environments, etc.

While the benefits are quite promising, the technique seems to suffer from a lack of research. There is the SICL paper that talks about adding it to Common Lisp, and the SBCL compiler which at it's bootstrapping phase works on creating it's own environment. There is also MIT scheme which has first class environments

With Juvix, we can explore these ideas a lot further, as we have many systems which facilitate this kind of reasoning. Three particular constraints come together for this.

1. We have an algebraic effects system

   • This is very significant for making progress, as we can see precisely how our effects touch the image. If we can determine that, we can likely create a system that can precisely denote the scope of the image we need to reason over.

   • With that said, we need to be careful with our thoughts here, as free variables are an effect that are discharged by the default handler. Meaning that if the system fully throws this information away as it can lookup in the image what answers are bound to and throw away what it relies upon in the image to function, then this will be harder to manage.

2. We have multiple backends we must support in a single program.

   • This means that we already have to tackle the issue of some parts of our language being out of scope.

   • We are likely to include parts of Racket's #lang research, which should help talking about environments on a module level.

3. We have a first class module system.

   • We might be able to formalize this idea as our module system, or view it as an extension of our module system.

   • After all the image is one big module!

If we are able to synthesize 1., 2., and 3. properly along with our type system, we should have a very ergonomic way of creating very eloquent systems that can talk about library versioning, backend support, and evaluation time processing.

Subtyping is an important part of any module or object system. The rules these systems usually care about revolve around the subtype of Records and Records in relation to functions.

  f0 : λX:>{x : int} -> x1 -> x2 -> x1
  f0 rec1 rec2 = rec1 { x = rec1.x + rec2.x}


  f1 : λX:>{x : int} -> X -> X -> X
  f1 rec1 rec2 = rec1 {x = rec1.x + rec2.x}


  f2 : λX:>{x : int} -> X -> X -> X
  f2 rec1 rec2 = {x = rec1.x + rec2.x}


  -- note that the t is opaque
  sig set : int -> {x : t,  type t, add : t -> t -> t}
  mod set x =
    type t = int
    add = (+)
    x
  end

  -- We include the set
  sig bag : int -> {x : t,  type t, add : t -> t -> t}
  mod bag x = include (set x)

  foo a b c =
    let ab = a in
    ...

   foo1 a b c =
     let ab = new bag in
     ...


  f3 : λX:>{x : int} -> X -> -> X
  f3 rec1 = rec1 {x = rec1.x + rec1.x}

  λX:>bag X -> X -> X

  λX:>bag X -> X -> bag

  f1 {x = 5; y = 3} {x = 1}

  f3 {x = 3; y = 4}

  f1 {x = 5; y = 3} (coerce {x = 1})

  -- or
  f1 (coerce {x = 5; y = 3}) {x = 1}

Overall the goal of the S-expression incantation is twofold ¹.

1. An unambiguous syntax that is faithful to the original ML syntax

   • This is a necessity to have limited strife between the ML syntax. and the work we need to do on the generic IR-syntax layer.

   • Unambiguous in this case implies bijection, as we have to convert between the two forms.

2. A fully realized syntax that is readable and looks as if it were a standalone language.

   • This is needed so inspection of the output is obvious. Further this will empower ease of reasoning over the syntax without too many surprises.

• Overall a few forms in this representation are quite verbose and thus harder to read than they should be, see

  
    (:arrow
     (:infix : hd
             (:infix -> x
                     (:infix : cdr
                             (:infix -> (foo y) (foo x y z))))))
  
    ;; should be
    [ hd : x -> cdr : (foo y) -> (foo x y z) ]
  
    (:record
     y-axis y
     x-axis x
     z-axis z)
  
    ;; should be
    {y-axis y
     x-axis x
     z-axis z}

• This is due to lacking reader macros at this level. Overall this can be largely improved in the future for better inspection (we thus will offer another level of inspection that can do away with the infix view!)

The syntax is heavily inspired from Common Lisp (CL). There are of course a plethora of changes, however some key concepts have survived through this transition.

Namely for adding extra property based information in declarations we got for an alist concept

  (type (foo :type (:infix -> typ (:infix -> typ typ))) (x y z)
     (Foo a b c))

which is taken directly from CL's defstruct construct.

Even naming conventions like defun are lifted directly from Common Lisp.

With that said, many forms (namely the lets) lack an extra set of parenthesis when in comparison to CL and the Schemer language.

  (let fi (x) (:infix + 3 x)
      (fi y))

  (let fi () 3
      fi)

This is due to us fully abusing the fact that we must represent non let blocks currently along with having a single expression each name is bound to.

There are likely inconsistencies between some of the forms. These should be removed as soon as possible. I have tried my best on this front, but likely some forms are inconsistent.

  (type (foo :type (:infix -> typ (:infix -> typ typ))) (x y z)
     (Foo a b c))

  (:defsig foo (:usage 0 (:infix -> int (:infix -> int int))))
  ;; should be
  (:defsig (foo :usage 0) (:infix -> int (:infix -> int int)))

Instead of giving each variant a section, we will instead note that Values relate to Terms, except instead of an Elim they have a Neutral.

Thus, it's an extension of Term.

Neutral is the same as Value, except we remove annotations from the possibilities

• This is the target that the context type should hold. However we have to note a few facts about how things are stored.

• We don't really have ML syntax counterparts for these, so instead we will give the raw structure as the syntax.

Currently the capability library only displays each field of a record as an effect. Ideally we'd have effects explain certain kinds of computation instead, and logically bundle these fields into some kind of greater effect.

Tomas has brought to my attention of the eff library which may some day replace or aid our usage of capability.

• 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