Type Checker for Marlowe

[paluh]

In Marlowe, there is a sense in which we simulate dealing with only two variable types, distinguishing them by language constructs (Observation vs Value). However, it appears that Value encapsulates at least three distinct types that should be fully inferrable from the context and type-checkable: Timestamp, Amount, and the regular scalar Integer (probably we can even go further and distinguish currencies etc). This differentiation of types could lead to new types, such as TimeDuration, and should entail some form of typing for arithmetic operators and similar entities.
Type checker should of course also easily catch unbound variables errors etc.

[hrajchert]

If we think of Marlowe Core as an assembly language, then I wouldn't add a typechecker at that level. For an eventual expansion of Marlowe Extended Syntax with better constructs (functions, modules, etc) then I would definitively add it there (including the asset checking).

Note that Faustus, which is still under development, is a competitor/alternative to the Marlowe Extended Syntax and already has a type checker

[paluh]

If we think of Marlowe Core as an assembly language, then I wouldn't add a typechecker at that level.

I don't think about Marlowe as assembly language. I think about it as simple (so "easy" to analyse) "core language" which should have simple semantics and tools which give strong guarantees. I also think of Marlowe as something useful on its own - you should be able to write contracts in it.

• Marlowe is advertised as secure by providing tooling which help developer spot the problems.
• Marlowe encourages people to generate it from other languages (by providing JSON spec etc.). These languages should not care about type checking Marlowe themselves.
• We provide some static analysis around Marlowe. Don't we want to add another complementary approach like fully infereable type checking which could be in many cases faster and detect other weaknesses?

Note that Faustus, which is still under development, is a competitor/alternative to the Marlowe Extended Syntax and already has a type checker

Haskell and Plutus are languages with type checkers as well but they preserve type checking on the core level on purpose - to prevent compilation and typing bugs on the upper layers.
Additionally Faustus is probably a long way to go. People are starting to use Marlowe right now.