Higher order functional language typing in prolog.
The program reads a typeable HOFL term and assigns types to it producing a LaTeX representation.
There are also auxiliar predicates for capture-avoiding substituitions, free variables, canonical form derivation, canonical form checking
The actual syntax differs by:
- lambda is replaced by a backslash \
- multiplication symbol is *
τ ::= int | τ0 * τ1 | τ0 → τ1
types are assigned to pre-terms using a set of inference rules (structural induction of HOFL syntax)
Type rules are used to derive type constraints (type equations) whose solutions (via unification) define the principal type.
We assign semantics only to terms that are well-formed and closed.
Requirements:
- SWI-Prolog
Usage:
$ swipl hofl.pl <?opts> ?term
To avoid possible errors with the prolog syntax it is recommended to write the term as a string (i.e. "term")
Flag | Type | Description |
---|---|---|
-h, --help | show the help message | |
-m, --mode | Atom | Modes are: - canonical: derive the canonical form - typing: assigns types to a term |
-f | Atom | read term from <path> |
-o | Atom | write output (typing) to <path> |