Desugaring applications of type constructors

[ciaran-matthew-dunne]

Hello again,

What is the official policy for desugaring applications of type constructors?

In my translation of Eunoia specs to LambdaPi, I have adopted the useful policy of desugaring 'object-level' applications to the _ operator. I consider applications of programs and builtins to be 'meta-level' applications, and so these stay n-ary.

For example: when translating the program $is_app, the term ($get_arg_list_rec (f x) acc) desugars to ($get_arg_list_rec (_ f x) acc).
This 'mixed' elaboration policy is nice for me for reasons that I won't explain here (although I'm happy to provide more details upon request).

For example, consider elaborating the term (@pair U T)).
First, note the _ constant must have the following (parameterized) type: (-> (-> X Y) X Y) where X and Y are implicit parameters of type Type.
A naive desugaring may give (_ (_ @Pair U) T).
But this is ill-typed because @Pair has type (-> Type (-> Type Type)) (recognizing that -> is right-associative) and U and T both have type Type. So there is no way to unify (-> X Y) with (-> Type (-> Type Type)), because this would require Type : Type, which is known to be inconsistent in 'sufficiently powerful' type systems.

So I come to the conclusion that applications of type constructors (e.g., ->, @Pair, BitVec) must be desugared similarly to 'meta-level' applications. This is difficult (especially in the absence of declare-type), because such constants have the same formal status as 'term-level' constants.
So one needs to detect on-the-fly which constants are type constructors in order to desugar everything correctly. This essentially requires me to implement a type inference algorithm, which is something I was hoping to avoid.

Thanks in advance!

[ciaran-matthew-dunne]

On reflection, I realize that this may be simpler than I initially thought.

Symbols introduced to the signature by define should be considered computational. Therefore because @Pair is a defined symbol with definiens @@Pair, the application (@Pair U T) remains n-ary. In contrast, an application of @Pair (which is introduced by declare-const) such as (@Pair U T) would elaborate to an ill-typed term (_ (_ @Pair U) T).

However, it follows from this policy that applications of eo::List::cons and @list have identical desugarings, since eo::List::cons is 'computational', and @list is just a macro for the eo::List::cons. This means that (in the absence of ad-hoc mechanisms) programs whose rules match on arbitrary applications of constants (like eo::is_list_rec) would not operate on lists constructed by @list, because the pattern ($eo_is_list_rec f nil (f x y)) desugars to ($eo_is_list_rec f nil (_ (_ f x) y)), but the term like (@list z zs) would just desugar to itself.

Is this the intended behaviour?

Best wishes,
Ciarán

[hansjoergschurr]

Hm, I am not sure I follow the entire train of thought here, but let me write some thoughts:

First, Eunoia does assume Type : Type. The reason is that we don't care about consistency. Eunoia is not a "proofs as program" system, and you can trivially define inconsistent rules (in whatever calculus you model). Instead, it is more of a scripting language to script a proof checker. We do, however, want type safety.

Second, I don't think _ is a proper language constant with a type. It is merely a syntactic convenience, because SMT-LIB doesn't allow the first element of a list in an S-expression to be a list. That is, ((f a) b) is not legal SMT-LIB. So you can't write typical higher-order function application and the _ is the hack to get around it: (_ (f a) b) is syntactically valid.