Typed Exprs

Typed Expressions in Drasil

Basic Background Information

• Drasil is a system of knowledge-oriented programming languages, and a compiler for said languages.
• Drasil is bootstrapped in Haskell.
  • Eventually, Drasil will be built in Drasil.

Objective

Expressions should be well-typed, and expose information about their resultant types.

Specifically, we would like the terms of the Expression language to be "safe" in usage, so that we can reliably generate well-formed and well-behaved programs.

Solution: Forming a system of constraints for expression formations

In order to ensure that all terms of the expression language are "valid"/well-formed, we must define what it means for any term to be "valid"/well-formed. We will define "validity"/well-formedness here through defining a system of inference rules that dictate when we're able to form terms of the expressions abstract syntax tree.

The Inference Rules

TODO: inference rules & syntax chart as done in "Practical foundations for Programming Languages" (e.g., Harper, pg. 34). Export to SVG(?) and link here.

Major Design Choice: Phase distinction for type checking

TODO: discuss phase distinction

Leaning on Haskell's type system

Prototype

Prototype of notable problem: unable to automatically collect and apply a function to all things of a specific type constructor, ignoring its type arguments, due to being unable to disambiguate the type arguments

TODO: discuss

Pros

• TODO:

Cons

• TODO:

Rolling our own type system

Prototype

TODO: discuss

Pros

• TODO:

Cons

• TODO: