Documentation

Type-indexed constants. These include both language built-ins (if, arithmetic, comparison, <>, etc.) as well as combinators (S, I, C, K, B, Φ) we will use both for elaboration and later as a compilation target.

Type-level list append.

Type- and context-indexed de Bruijn indices. (v :: Idx g a) means v represents a variable with type a in a type context g.

A variable valid in one context is also valid in another extended context with additional variables.

Type-indexed terms. Note this is a stripped-down core language, with only variables, lambdas, application, and constants.

A term valid in one context is also valid in another extended context with additional variables (which the term does not use).

Errors that can occur during typechecking/elaboration.

Base types.

Type representations indexed by the corresponding host language type.

Check that a particular type has an Eq instance, and run a computation in a context provided with an Eq constraint. The other checkX functions are similar.

Wrap up a type-indexed thing to hide the type index, but package it with a TTy which we can pattern-match on to recover the type later.

Type contexts, indexed by a type-level list of types of all the variables in the context.

Look up a variable name in the context, returning a type-indexed de Bruijn index.

Check that a term has a given type, and if so, return a corresponding elaborated and type-indexed term. Note that this also deals with subtyping: for example, if we check that the term 3 has type World Int, we will get back a suitably lifted value (i.e. const 3).

Get the underlying base type of a term which either has a base type or a World type.

Apply one term to another term, automatically handling promotion and lifting, via the fact that World is Applicative. That is, (1) if a term of type T is used where a term of type World T is expected, it will automatically be promoted (by an application of const); (2) if a function of type (T1 -> T2 -> ... -> Tn) is applied to any arguments of type (World Ti), the function will be lifted to (World T1 -> World T2 -> ... -> World Tn).

Infer the type of an operator: turn a raw operator into a type-indexed constant. However, some operators are polymorphic, so we also provide a list of type arguments. For example, the type of the negation operator can be either (Int -> Int) or (Float -> Float) so we provide it as an argument.

Currently, all operators take at most one type argument, so (Maybe SomeTy) might seem more appropriate than [SomeTy], but that is just a coincidence; in general one can easily imagine operators that are polymorphic in more than one type variable, and we may wish to add such in the future.

Given a raw operator and the terms the operator is applied to, select which types should be supplied as the type arguments to the operator. For example, for an operator like + we can just select the type of its first argument; for an operator like if, we must select the type of its second argument, since if : Bool -> a -> a -> a. In all cases we must also select the underlying base type in case the argument has a World type. For example if + is applied to an argument of type World Int we still want to give + the type Int -> Int -> Int. It can be lifted to have type World Int -> World Int -> World Int but that will be taken care of by application, which will insert the right combinators to do the lifting.

Typecheck the application of an operator to some terms, returning a typed, elaborated version of the application.

Infer the type of a term, and elaborate along the way.

Try to resolve a RawCellVal---containing only Text names for terrain, entities, and robots---into a real CellVal with references to actual terrain, entities, and robots.

Try to resolve one cell item name into an actual item (terrain, entity, robot, etc.).

Infer the type of a let expression, and elaborate into a series of lambda applications.

Infer the type of an overlay expression, and elaborate into a chain of <> (over) operations.