Amulet, now with high-effort error messages.
@amiloradovsky much like present-day Haskell, we don't have dependent types, but one can fake them by clever use of GADTs (see, e.g., https://hydraz.semi.works/txt/vector.ml.html and https://hydraz.semi.works/txt/lambda_term.ml.html).
I have unsuccessfully tried to add full dependent types in the past, and do consider trying again, but considering how tough the implementation is, I'm not sure if it'd be worth it.
Most of our effort right now is in making the compiler more correct and making generated code more efficient.
@hydraz
Do you have a (multi-parameter) type-classes then (for implementing, e.g., affine/vector spaces, or, say, fiber bundles)?
@amiloradovsky Ahh, you've called my bluff. No, not yet—we want to implement (multi-param) type classes using implicit modules, and that requires, well, a module system.
However, I'm a bit burned out from working on the type checker, so I've been putting it off :/
@amiloradovsky Amulet has less of a focus on decent support for imperative programming (mutable records, etc) than O'Caml, and barely no module system when compared to Standard ML.
Our type system is based on several of the papers behind GHC's implementation, which means that we can type (roughly) the same definitions as GHC Haskell - for the features we support, of course - there are no type functions, or promoted kinds, for instance.