System FC

System FC is the typed core language of AIHC. The FC modules desugar the type-checked surface tree into System FC. The optimizer works on System FC. Then, the GRIN modules lower System FC to GRIN.

The code is in bin/aihc/compiler/fc/src/Aihc/Fc/. The design document is docs/system-fc.md.

Properties

System FC is similar to Haskell, but it has no syntactic sugar and no ambiguity.

• Each binder has a type. A use of a binder has no type.
• Each type argument is explicit, for example f @tInt.
• Each class constraint is an explicit dictionary argument. A class becomes a data type with the name $Dict$Class.
• A case expression has an optional case binder and at least one alternative. The first alternative gives the result type. All alternatives must have the same result type. An alternative type variable must not occur free in the result type.
• A literal expression has its full type and runtime representation. For example, lit (1#cIntRep) :: tInt#.
• An empty case becomes absurd e return (T). This expression evaluates e and reports a match failure if evaluation returns. Its result type is T.
• A newtype becomes a type and an axiom. A cast e ▷ γ changes the type of an expression with a coercion γ.
• Types and kinds are one language. The function arrow → is FUN on lifted types.
• The FC lint checks the types of a program again. Use --lint to run it.

Names

Each name has a scope number and a prefix. The scope table at the start of a file gives the package and the module of each scope number. The prefix gives the sort of the name.

Prefix	Sort	Example
t	Type constructor	12.tInt
s	Type synonym	12.sType
c	Data constructor	12.cI#
v	Value	5.vprint

A local binder has no prefix. If a local binder has the same name as an outer binder, the printer adds a number, for example x{1}.

Top-level forms

Form	Meaning
scope N = "package" Module	A scope number for the names of one module.
import headers	The types of the imported names that the module uses.
type T :: kind { constructors }	A data type and its constructors.
val x :: type = expression	A top-level value.
pub	The module exports the declaration.
axiom	An axiom, for example for a newtype or a type family instance.

Example

This module has a recursive function on lists:

module Example where

append :: [a] -> [a] -> [a]
append [] ys = ys
append (x : xs) ys = x : append xs ys

The compiler makes this System FC program for the module:

scope 1 = "" Example
scope 2 = "aihc-prim" GHC.Types

import headers
  constructors [2.cLifted, 2.cUnlifted] 2.tLevity :: sType;
  2.sLiftedRep :: tRuntimeRep;
  constructors [2.cAddrRep, 2.cBoxedRep, 2.cDoubleRep, 2.cFloatRep, 2.cInt16Rep, 2.cInt32Rep, 2.cInt64Rep, 2.cInt8Rep, 2.cIntRep, 2.cSumRep, 2.cTupleRep, 2.cVecRep, 2.cWord16Rep, 2.cWord32Rep, 2.cWord64Rep, 2.cWord8Rep, 2.cWordRep] 2.tRuntimeRep :: sType;
  2.tTYPE :: ∀(rep : tRuntimeRep). sType;
  2.sType :: sType;
  constructors [2.c[], 2.c:] 2.t[] :: ∀(a : sType). sType;
  2.c: :: ∀(a : sType). a → t[] a → t[] a;
  2.cBoxedRep :: tLevity → tRuntimeRep;
  2.cLifted :: tLevity;
  2.c[] :: ∀(a : sType). t[] a

import synonyms
  2.sLiftedRep = cBoxedRep cLifted;
  2.sType = tTYPE sLiftedRep

pub val 1.vappend :: ∀(a : sType). t[] a → t[] a → t[] a
  = Λ(a : sType). λ(x : t[] a) (y : t[] a).
    case x of {
      c[] →
        y;
      c: (x{1} : a) (xs : t[] a) →
        c: @a x{1} (vappend @a xs y)
    }

The compiler made these programs at the default optimization level. The Lir is for the target linux-amd64.

The page Examples shows more programs.