pure
pure copied to clipboard
CakeML
A verified compiler for a lazy functional language
The following is the proposed sequence of optimisations for ThunkLang. The actual implementation might merge a few of these. 1. pure-to-thunk incorporates let-force (unlike now) 2. pull lam out of...
GADTs (generalised algebraic data types) can be quite a useful feature, but we must ensure we can infer their types effectively. Suggested by QuviQ.
We do not currently permit type synonyms, e.g. `type syn = old_type`. Suggested by QuviQ.
Users may assign unwanted values to underscores ("don't care"). We should support this feature too. Suggested by QuviQ.
We lack left-hand side pattern matches (both for `let` bindings and function clauses), deep pattern matches, and guarded pattern-matches. This issue will track discussion around these features. Suggested by QuviQ.
Currently everything is a "parse error". We should plumb through at least basic error reporting.
Type inferencer ignores type signatures. Example: ``` foo :: String -> Int -> UndefinedType -> [Bool] foo i = () main = Ret (foo 1) ```
The compiler accepts this: ``` l1 ++ l2 = case l1 of [] -> l2 h:t -> h : (t ++ l2) main = Ret () ``` But rejects any...
This works: ``` data Error = Fail main = Raise Subscript ``` While the following is rejected by the compiler: ``` data Error = Fail main = Raise Fail ```
Issue https://github.com/CakeML/pure/issues/27 ensures that most dead code still gets type-checked. However there are still [problems](https://github.com/CakeML/pure/issues/27#issuecomment-1466223902) with multiple declarations of the same name due to the [`letrec` distinctness pass](https://github.com/CakeML/pure/blob/65f55650c57cd04e5cd36f0aed2c9e59faf00252/compiler/backend/passes/pure_letrec_cexpScript.sml#L105). Also, the...