SydML's Core

Core is an explicitly-typed IL based on System F_ω.

Definition

e ::= x                     Variables
   |  λx:τ. e               Term abstractions
   |  Λx:κ. e               Type abstractions
   |  e e                   Term applications
   |  e @τ                  Type applications
   |  let x = e in e        Let-bindings
   |  letrec (x = e)* in e  Recursive let-bindings
   |  case x of {P → e}*    Case-expressions

τ ::= K                     Type constructors
   |  τ τ                   Constructor application
   |  τ → τ                 Function types
   |  ∀x:k. τ               Universal quantification

k ::= Type                  The kind of all types
   |  k → k                 Higher kinds

Use of the pass parameter

Core's most notable use of the pass parameter is to share the same AST for typed and untyped Core.

data TermF p e
  = AbsF Name.UniqueName e
  | TyAbsF !(PassTyAbsFAnnotation p) Name.UniqueName e
  | AppF e e
  | TyAppF e !(PassType p)
  | CaseF e (List (CaseAlt p e))
  | ValF Value

-- | Setting these two extension points to Void completely disables the
--   constructors.
type Untyped p = (PassType p ~ Void, PassTyAbsFAnnotation p ~ Void)