Static typing

[0x0f0f0f]

Implement static typing for expressions and function:

• [x] An ADT representing type representations, with an additional number type that includes all the numerical tower types
• [ ] Get all the type info into that type
• [x] A function that infers an expression type
• [ ] Complete this function
• [ ] Include type information in closures
• [ ] Infer function types automatically, automatically using a generic number type if not strictly imposed.
• [ ] Extend abstract and concrete syntax with haskell-style type annotations

[chrisnevers]

I'd like to work on this issue. I can implement a constraint based type inference algorithm, that's easy to learn & extend

[0x0f0f0f]

Thank you! :D Do you have any material to read about this kind of inference algorithms? I may also use your ocamline library for #8

[chrisnevers]

Nice, thanks for choosing ocamline! 🎉 I'm using an approach described by Matthew Flatt's book Programming Language and Lambda Calculi from Chapter 16

[0x0f0f0f]

Also: Should static and dynamic typing be mixed? Like introducing a type for statically typed Lambdas.

• [x] Keep an additional value in functions' type information telling if the function contains impure primitives or blocks (purity) and if it is pure, if it is numerical or not (because it can tell if the function can be differentiated or integrated)

[chrisnevers]

What's the use case for mixing static and dynamic typing? How would an expression be marked as dynamic (To inform the compiler not to perform inference on it)?

[0x0f0f0f]

I think the opposite (dynamic by default) should be the best usage case. Static functions may be defined with the concrete syntax sfun x y z -> body or slambda. We have to see if mixing static and dynamic typing is appropriate, or if migrating to static typing completely is the best option. If we migrate to static typing completely, we should find a way to decide how arguments are passed to primitives.

In dynamically typed functions, I'd like inference to be separated in two different steps, one infers the purity of an expression (Impure, Pure or Numerical which is only numerical computations and will be needed for differentiation). The other step makes normal type inference.

Type inference should be performed before normalization (optimizer.ml). I think the order that makes most sense is infer type -> normalize expression -> infer expression purity -> evaluate if purity is appropriate

• [x] A function that infers the purity of expressions

[0x0f0f0f]

This is my first and really naive approach to inference: this function infers if an expression contains pure, impure or numerical code. Note that numericality depends on parameters. https://github.com/0x0f0f0f/minicaml/blob/157fed56c12ecda628b70ee04b73ffc4583ae614/lib/typecheck.ml#L61-L107

This is how i avoid repeating inference when evaluating expressions that have a nested body: eval now accepts a labeled argument with default value called knownpurity. If the purity of a nested expression is known, do not calculate it again. https://github.com/0x0f0f0f/minicaml/blob/157fed56c12ecda628b70ee04b73ffc4583ae614/lib/eval.ml#L25-L37

Please tell me if you have any suggestions! 🥂😀

[0x0f0f0f]

I will keep gobba dynamically typed for the time being.