I've been building an implementation of the "Sound and Complete" type system, as those of you who follow me on Twitter might know (hi!), and I'm fairly close to finishing the system of the paper.
I intend to extend it with support for the two things mentioned in the ending "Extensions" section:
-
constructors that take arguments
-
recursive types (like
[ ])
and use it as a Core language for a new Haskell-like language. But I'm implementing an evaluator at present, as being able to "run" small programs is pretty motivating.
What evaluation strategy I should use?
I'm leaning towards not using strict evaluation: all 2.5 recent "alt-Haskells" (PureScript, Idris, and Sixten) are strict(-by-default; Idris has Lazy), so, if nothing, there's the "I want to try something else" argument. This could also potentially help us get some more interesting Haskell interop than just going through the C FFI.
The paper's treatment of recursive expressions only allows fixed points of values (~things in normal form), so, for instance, one can write something like rec x. v where v is a value, e.g.
rec foo. \x -> case x of 0 -> 1; _ -> 2 * foo (x - 1)
which is the equivalent of the Haskell expression
let
foo 0 = 1
foo x = 2 * foo (x-1)
in foo
The paper says "values v are standard for a call-by-name semantics".
Q1. The rec x. v form is equivalent to fix, I think: rec x. v is fix (\x -> v), isn't it?
Q2. Does this also give us mutually recursive lets, by desugaring let x = f y; y = g x; in body to the following?
case rec p. (f (fst p), g (snd p)) of (x,y) -> (\x y -> body) x y
Q3. The language as it stands doesn't have let, but it does have case. Is there anything wrong with treating let Con c = rhs in body as case rhs of Con x -> (\c -> body) x for the purposes of type-checking (thinking of lets as case-expressions with a single branch), but otherwise treating let separately for evaluation purposes?
Q4. What resources would you recommend for implementing a call-by-need language?
Q5. Just putting this out there: any thoughts about optimistic evaluation? It's significantly complex, but a language using it as the primary evaluation model could be interesting.
As a Haskell user, non-strict evaluation is great when
Resorting to manual strictness annotation is difficult in Haskell because the propagation of strictness is not manifest. It occurs to me that one solution to this problem would be to treat strictness/non-strictness as an annotation on types. Strictness analysis would be replaced by inference and bang-patterns would be replaced by type signatures. The user and compiler can dialog about strictness with it reflected at the type level.