NOTE: dependent type language

This is a brief note about what a type theory should have and the flow.

1. Top level

A top level of dependent type language should be a modular thing, whatever a module or big letrec. In the top level, we should be able to have a list of definitions, these definitions should be able to reference each others. We will need an independent context for these, and use elaboration to break them down into core AST.

1.1. Elaboration

This step converts top level definition like data=(inductive family), =let, or letrec into a set of bindings from identifier to the core term. For example

inductive data type
let is definition that will not recursively refer to self and with syntax like let var : type = term, hence, we could apply function check from check component
1. check term type ensure the term has type
2. extends the global context
  - var to type in type context(or record type information in value, I'm not sure it's always work)
  - var to term in value context
letrec will refer to self, this is important feature when implementing function
introduce de Bruijn indices as local context?

2. Check component

This component should verify

checkType term: given term is a valid type
check term type: given term has type
1. infer type of term produces tm_type
2. invokes equateType type tm_type

3. Inference component

Produces a type from a term

4. Equate component

This component should verify

equateType context type tm_type: normalized types are same under the context
equate context value value: values are same under the context

5. Evaluate component

This component should produce value from term, for example, converts below

M : \Pi (x : A). B[x]
---------------------
    M(C) : B[x\C]