Add type annotations in rules ?

[francoisthire]

We have a PR (https://github.com/Deducteam/Dedukti/pull/172) in Dedukti which allows type annotations in rule contexts. If the annotation is not correct according to the type checker, then an issue is raised.

Another PR (https://github.com/Deducteam/Dedukti/pull/173) does the opposite, meaning it forbirds any annotation in rules.

Which feature is the one that Lambdapi aims to implement? In the old syntax, none of these behaviors is implemented. Annotations are allowed, but it could be anything.

[fblanqui]

Currently, in LP:

• in the old syntax, variable type declarations are ignored, as it was the case in Dk
• in the new syntax, there are no type declaration for variables What's the point of checking the correctness of type declarations? If there's no good example of this, we won't add this in LP.

[francoisthire]

I think it is the same idea than in OCaml when you write:

let f : int -> int -> int = fun x y -> x + y

instead of

let f = fun x y -> x + y

It is not necessary, but it might be helpful to debug a program. Especially, when the type checking algorithm of Lambda pi allows ill-typed patterns. Sure, there is a warning most of the times, but putting annotations could be helpful to debug a program. This is not a concrete example sure, but it gives some motivations at least.