chickadee » static-modules » make-core-typing

(make-core-typing type-term kind-deftype check-valtype check-kind valtype-match deftype-equiv kind-match deftype-of-path) procedure

This procedure creates the structure describing base language type checking. The meaning of the fields is as follows:

  • type-term: the main typing function, which takes a type and an environment, and returns the principal type of the term in the given environment
  • kind-deftype: infers and returns the kind of the given definable type
  • check-valtype check-kind: check the well-formedness of type and kind expressions in the base language
  • valtype-match deftype-equiv kind-match: checking values vs. signatures
  • deftype-of-path: transforms a type path and its kind into the corresponding definable type