Skip to content

Typed Exprs

Jump to bottom
Jason Balaci edited this page Feb 16, 2022 · 13 revisions

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.

Omitted for now, many are "obvious", but I will write them out properly soon™.

Major Design Choice: Phase distinction for type checking

An important thing to remember is that, ultimately, Drasil is a compiler on its own. Presently, Drasil and the ASTs of Drasil programs are bootstrapped in Haskell as a host language. In the future, Drasil might become a self-hosted compiler (and likely would need to be for Drasil in Drasil).

Since Drasil is bootstrapped in Haskell, we might find ourselves (as I have) looking to advanced Haskell tools to build Drasil. This might be great, and work great, but it would pose a problem later when trying to build Drasil in Drasil.

Here, we define the expression languages using an Algebraic Data Type in Haskell. In order for us to impose typing restrictions in Haskell, we may lean on Haskell's type system (e.g., leveraging GADTs), or we can roll our own type system for the expressions using .

Leaning on Haskell's type system

Prototype

Relevant Snippet:

var1 :: QuantityDict Int
var1 = mkQuantityDict (Proxy @Int) (mkUid "var1") "a1" "b1"

var2 :: QuantityDict Bool
var2 = mkQuantityDict (Proxy @Bool) (mkUid "var2") "a2" "b2"

func1 :: QuantityDict (Int -> Int)
func1 = mkQuantityDict (Proxy @(Int -> Int)) (mkUid "func1") "c1" "d1"

func2 :: QuantityDict (Bool -> Int -> Int -> Int)
func2 = mkQuantityDict (Proxy @(Bool -> Int -> Int -> Int)) (mkUid "func2") "c2" "d2"

varDef1 :: QDefinition Expr Int
varDef1 = mkQDefinition (mkUid "varDef1") var1 (int 1) "e1" "f1"

varDef2 :: QDefinition Expr Bool
varDef2 = mkQDefinition (mkUid "varDef2") var2 (not_ $ bool False) "e2" "f2"

funcDef1 :: QDefinition Expr (Int -> Int)
funcDef1 = mkQDefinition (mkUid "funcDef1") func1 (lam $ \x -> add x (int 1)) "g1" "h1"

funcDef2 :: QDefinition Expr (Bool -> Int -> Int -> Int)
funcDef2 = mkQDefinition (mkUid "funcDef2") func2 (lam $ \b -> lam $ \x -> lam $ \y -> ifTE b x y) "g2" "h2"

funcDef3 :: QDefinition Expr (Int -> Int)
funcDef3 = mkQDefinition (mkUid "funcDef3") func1 (lam (\x -> add x (int 1))) "g3" "h3"

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

Pros

  • Traceability of errors: Haskell reported errors are very descriptive and easy to read, showing the specific line numbers and files that a problem occurs.
  • Readability: Types of Quantities, Definitions, etc. are displayed elegantly through the type arguments of the Haskell variables.

Cons

  • Named arguments in function calls do not play well statically.
  • Relies heavily on "upgraded" ChunkDBs.
  • Types of the literals show up with Haskell names, instead of the preferred names (the ones used in the Space ADT).
  • Dictating the space/type of a quantity relies on either Type Applications or on Proxy. Either way, it relies on something that is very deep in Haskell.

Rolling our own type system

Prototype

Relevant Snippet:

var1 :: QuantityDict
var1 = mkQuantityDict S.Integer (mkUid "var1") "a1" "b1"

var2 :: QuantityDict
var2 = mkQuantityDict S.Boolean (mkUid "var2") "a2" "b2"

func1 :: QuantityDict
func1 = mkQuantityDict (S.Function (S.Integer NE.:| []) S.Integer) (mkUid "func1") "c1" "d1"

func2 :: QuantityDict
func2 = mkQuantityDict (S.Function (NE.fromList [S.Boolean, S.Integer, S.Integer]) S.Integer) (mkUid "func2") "c2" "d2"

varDef1 :: QDefinition Expr
varDef1 = mkQDefinition (mkUid "varDef1") var1 (int 1) "e1"

varDef2 :: QDefinition Expr
varDef2 = mkQDefinition (mkUid "varDef2") var2 (not_ $ bool False) "e2"

Pros

  • As rules are explicitly written, we have generally more flexibility in our type system.
    • Allows for named arguments in function calls.
  • This prototype can likely be implemented directly in existing Drasil infrastructure.
    • Additionally, at a glance, looks like it would work without the "upgraded" ChunkDBs. However, having Typed UID references is a large bonus, we can likely make this an aside issue bringing discussion of chunk formation into question as well.
  • Giving quantities a type/space is done normally through QuantityDicts.

Cons

  • If an expression is ill-formed, and since Haskell is lazy-evaluated, we will likely only find out at some point during the runtime (Drasil's compile-time). In other words, we would not be able to leverage Haskell Language Server to statically find errors as we write expressions (though, we could write our own LSP if we really wanted it later [/largely down the road]).
  • Haskell's type system is very rich and works well for most things.
  • Readability in Haskell is a bit difficult to trace.
  • Traceability of errors (due to errors only being thrown at runtime, we would need to display UIDs to be able to locate problematic areas).

Potential Changes

  • "error" usage might make things a bit difficult, perhaps we can switch to using more Either Expr Error (with type Error = String/Text)?
  • Add support for higher order expressions functions (doesn't look too difficult with this style!)
  • Dummy variables instead of using registered QuantityDicts for parameters

Future

  • Types and type constraints might be better to be written as ideas in Drasil as well, using a Haskell stub as the runtime.

Other Decisions

  1. Should symbol references be to specific implementations of a symbol? As of right now, we are going against this.
Clone this wiki locally