This note summarizes what Juvix can learn from the implementation of Idris 2. References:
- The paper.
- Scottish summer school 2020 slides/notes.
- Video lectures of the summer school.
- The implementation documentation.
Idris 2 represents linearity with the following syntax:
- (0 x : T) for arguments that are only used in compile time and never used in run time (type information). These arguments are erased at run time.
- (1 x : T) for arguments that are only used in run time once.
- (x : T) for an argument which is usable with no restrictions. That is, arguments without annotations of '0' or '1' have ω usage.
It is valid to use an argument with multiplicity ω in a position with multiplicity 1. A linear argument is a promise that the function will use the argument exactly once, not a requirement that the argument is not used elsewhere.
Relatedly, linearity is specified in functions, not in data type definitions. A data type should have no usage restriction on its own.
For efficiency, proofs generally have 0 usages to indicate that it is not needed in run time. As a result, we get a safe-guard almost for free as there is no cost at run time.
Implicit arguments are resolved by unification. Idris 2 also supports auto-implicit
arguments, which are resolved by searching for a unique expression of the appropriate type,
using data constructors and local variables as search hints, as well as explicitly declared hints. For example, we can write a total fromMaybe function as follows:
data IsJust : Maybe a -> Type where
ItIsJust : IsJust ( Just val )
fromMaybe : ( x : Maybe a ) -> { auto p : IsJust x } -> a
fromMaybe ( Just x ) { p = ItIsJust } = xThe notation {auto x : T} -> ... declares an auto-implicit argument, which can be
annotated with multiplicities like other implicit and explicit arguments. When we apply
fromMaybe to an argument, the type checker will try to find an appropriate implementation
of IsJust. This will succeed if the value is of the form Just val, and fail otherwise:
Main > fromMaybe ( Just 10)
10
Main > fromMaybe Nothing
( interactive ):1:1 -- 1:18: Can ’ t find an implementation for
IsJust Nothing
The auto-implicit implementation in Idris 2 consolidates auto-implicit search and implementation search into the same mechanism, with the same notation.
Idris 2 (high level syntax)
-> (desugars to)
TTImp (intermediate type theory with implicits, interactive edition functions)
-> (elaborates to)
QTT (core type theory with quantities)
-> (compiles to)
CExp (untyped lambda calculus, erasure, inlining - Brady noted that this has huge efficiency gains)
-> (maps to)
Chez scheme
In TT (QTT without quantities), the terms are fairly standard but have dependent types. E.g., the bound variables (Local) have a proof that the index is valid in its input. This reduces mistakes e.g., from manipulating de Bruijn indices. However this is not readily available to us because Juvix is not implemented in a dependently typed language. However, there are a few implementation tricks that we may wish to follow:
- Add a data type that includes all the binders.
- parameterize to avoid lookups and mistakes (make the type checker work for you)
- parameterize the local environment to avoid term and scope mixups.
- heavily parameterize the global context.
- using
gluedterms to increase efficiency (the increase in efficiency is not formally proven)
See below sections for details.
Functions and lambdas are under Bind. Bind also includes pattern bound variables and their types. As we add pattern matching we may do the same for easier abstraction (e.g., map and traverse). E.g., we can add quantities to Bind, along with other manipulations that apply to all the binders.
Binders (Bind) are:
data Binder : Type -> Type where
Lam : PiInfo -> ty -> Binder ty
Pi : PiInfo -> ty -> Binder ty
PVar : ty -> Binder ty -- pattern bound variables ...
PVTy : ty -> Binder ty -- ... and their typeFunction definitions consist of a type declarations and pattern bindings. In the function clauses, variables are bound by pat binders (PVar).
Binders are terms:
data Term : List Name -> Type where
Local : (idx : Nat) -> -- de Bruijn index
(0 p : IsVar name idx vars) -> -- proof that index is valid
Term vars
Ref : NameType -> Name -> Term vars -- a reference to a global name
Meta : Name -> List (Term vars) -> Term vars -- meta-variables, used for unification
Bind : (x : Name) -> -- any binder, e.g. lambda or pi
Binder (Term vars) ->
(scope : Term (x :: vars)) -> -- one more name in scope
Term vars
App : Term vars -> Term vars -> Term vars -- function application
TType : Term vars
Erased : Term varsNote that the global variables have NameType as an argument. It indicates whether the term is a data or type constructor or function. It avoids a look up and yields a slight performance improvement.
Note also that they have Erased terms.
The type signature of environment in Idris 2 is heavily parameterized:
data Env : (tm : List Name -> Type) -> List Name -> Type where
Nil : Env tm []
(::) : Binder (tm vars) -> Env tm vars -> Env tm (x :: vars) -- this last term requires dependent typesOnly well-scoped terms with the list of names can be added to an environment and this is enforced by the first argument of Env. That is, an environment carries any terms with a well-scoped type. And the scope of each term is explained. An environment can also carry values instead of term. This has the advantage of avoiding mistakes of mixing up terms and their scopes.
As one add a binder (first input of (::)), the environment has one more variable in it, as reflected by the type signature Env tm (x :: vars). We may have to leave it as Env tm vars because Haskell doesn't natively support dependent types.
A global context contains (similar to Juvix):
- Type constructors
- Data constructors
- Function declarations and definitions
- holes (unknown types)
Also
- Guesses (definitions whose validity has not been checked. It's valid when certain unification constraints are satisfied - same implementation as in Agda).
Similar to the environment, the global context is heavily parameterized:
data Def : Type where
None : Def -- Not yet defined
PMDef : (pminfo : PMDefInfo) ->
(args : List Name) ->
(treeCT : CaseTree args) ->
(treeRT : CaseTree args) ->
(pats : List (vs ** (Env Term vs, Term vs, Term vs))) ->
-- original checked patterns (LHS/RHS) with the names in
-- the environment. Used for display purposes, for helping
-- find size changes in termination checking, and for
-- generating specialised definitions (so needs to be the
-- full, non-erased, term)
Def -- Ordinary function definition
ExternDef : (arity : Nat) -> Def
ForeignDef : (arity : Nat) ->
List String -> -- supported calling conventions,
-- e.g "C:printf,libc,stdlib.h", "scheme:display", ...
Def
Builtin : {arity : Nat} -> PrimFn arity -> Def
DCon : (tag : Int) ->
(arity : Nat) ->
(newtypeArg : Maybe (Bool, Nat)) ->
-- if only constructor, and only one argument is non-Rig0,
-- flag it here. The Nat is the unerased argument position.
-- The Bool is 'True' if there is no %World token in the
-- structure, which means it is safe to completely erase
-- when pattern matching (otherwise we still have to ensure
-- that the value is inspected, to make sure external effects
-- happen)
Def -- data constructor
TCon : (tag : Int) -> (arity : Nat) ->
(parampos : List Nat) -> -- parameters
(detpos : List Nat) -> -- determining arguments
(flags : TypeFlags) -> -- should 'auto' implicits check
(mutwith : List Name) ->
(datacons : List Name) ->
(detagabbleBy : Maybe (List Nat)) ->
-- argument positions which can be used for
-- detagging, if it's possible (to check if it's
-- safe to erase)
Def
Hole : (numlocs : Nat) -> -- Number of locals in scope at binding point
-- (mostly to help display)
HoleFlags ->
Def
BySearch : RigCount -> (maxdepth : Nat) -> (defining : Name) -> Def
-- Constraints are integer references into the current map of
-- constraints in the UnifyState (see Core.UnifyState)
Guess : (guess : ClosedTerm) ->
(envbind : Nat) -> -- Number of things in the environment when
-- we guessed the term
(constraints : List Int) -> Def
ImpBind : Def -- global name temporarily standing for an implicitly bound name
-- A delayed elaboration. The elaborators themselves are stored in the
-- unification state
Delayed : DefIn Juvix, we have a lot of the above input arguments in record fields instead.
Note that tag is an input to DCon and TCon (data/type constructors). When we implement it we should use Nat type because this tag should never be negative.
Every (data/type) constructor gets a tag associated with it, which is used as part of the case tree. The tag is dispatched rather than the name of the constructor. At run time the case expressions are compiled into a jump table, which is much faster.
Glued terms (see here)
When type checking a variable, we look up the variable in the environment/global context. Its type would be a value (Term vars). But it may be that we need to reduce it further to its normal form. So the type available is a value (NF vars). A glued term is constructed from either a Term or a NF, whichever is available. This allows lazy evaluation of terms to their normal forms - i.e., only convert when we need to.
Core is a IO monad where all of normalization, evaluation and conversion checking happen. This is a bit ugly (everything is done in IO) but required because this is more performant. When we load the representations in libraries (which are binary data), decoding them can be expensive. Instead of decoding all terms, we look up the terms that are actually used and do operations (read and write) of them via the global context (Def), in Core.
In Core.Value:
data NF : List Name -> Type where
NBind : FC -> (x : Name) -> Binder (NF vars) ->
(Defs -> Closure vars -> Core (NF vars)) -> NF varsUnification (Core.Unify and Core.UnifyState)
Unification concerns type checking with the presence of meta-variables. Meta-variables are variables with unknown values but type checking/elaboration progress could generate constraints that these variables have to satisfy and thus find the solutions to these variables. Implicit arguments are inferred by unification. See here for the implementation details. See also this video.
Pattern matching definitions are compiled to case trees for ease of compilation and coverage checking. See chapter 5 of The implementation of functional programming languages.
The compiled case trees appear in the global context in pattern matching definitions (PMDef).
data CaseTree : List Name -> Type where
||| case x return scTy of { p1 => e1 ; ... }
Case : {name, vars : _} ->
(idx : Nat) ->
(0 p : IsVar name idx vars) ->
(scTy : Term vars) -> List (CaseAlt vars) ->
CaseTree vars
||| RHS: no need for further inspection
||| The Int is a clause id that allows us to see which of the initial clauses are reached in the tree
STerm : Int -> Term vars -> CaseTree vars
||| error from a partial match
Unmatched : (msg : String) -> CaseTree vars
||| Absurd context
Impossible : CaseTree vars
||| Case alternatives. Unlike arbitrary patterns, they can be at most one constructor deep.
data CaseAlt : List Name -> Type where
||| Constructor for a data type; bind the arguments and subterms.
ConCase : Name -> (tag : Int) -> (args : List Name) ->
CaseTree (args ++ vars) -> CaseAlt vars
||| Lazy match for the Delay type use for codata types
DelayCase : (ty : Name) -> (arg : Name) ->
CaseTree (ty :: arg :: vars) -> CaseAlt vars
||| Match against a literal
ConstCase : Constant -> CaseTree vars -> CaseAlt vars
||| Catch-all case
DefaultCase : CaseTree vars -> CaseAlt varsSimilar to Agda's interactive editing support, Idris 2 has interactive editor support in Vim and other editors. Juvix should have similar support. According to Edwin Brady, a lot of work can be done via the REPL (at the TTImp level), which makes it easy to adopt to other editors. See the code for vim and emac editor support.
Idris and Idris 2 have successfully engage a relatively large community for a dependently typed language. I notice a few actions that may have caused the success:
- make it very easy for the community to contribute. They do so by maintaining good documentation and making implementation decisions that make it easy to contribute (e.g., as mentioned in the interactive development environment section).
- engage audiences through different channels. For example, blog posts may appeal to developers while working/publish academic paper may appeal to academic researchers.
Juvix can follow Idris's suit and engage a large community by various channels:
- present the implementation of the language in detail in various events. Similar to the SPLV2020 lectures
- maintain a friendly and detailed implementation documentation page similar to Idris 2's.
- publish a working paper detailing the implementation, similar to this.
- publish blog posts (already planned).