In Haskell, I can define a data type like

`data LC = App LC LC | Abs (LC -> LC)`

This isn't possible with `Inductive`

, as far as I know. What's the right way to model this in Coq?

There are lots of ways. One way is to switch to `data LC = App LC LC | Abs LC | Var int`

, with the last constructor representing a de Bruijn index. Another way is to use parametric higher-order abstract syntax.

Can you tell me more about the parametric higher-order abstract syntax?

Basically, it is `data LC = App LC LC | Abs (V -> LC) | Var V`

for an arbitrary type `V`

(hence the parametricity). But you should google it, as it is hardly something that can be explained in a few lines.

The point of the Haskell data type is that it leans on the native notion of function and substitution rather than defining it explicitly. Chlipala's "Parametric Higher-Order Abstract Syntax for Mechanized Semantics" and the earlier Despeyroux, Felty and Hirschowitz' "Higher order abstract syntax in Coq" both avoid negative occurrences rather than build a non-inductive type:

The first obstacle is that negative occurrences of the type being defined are not allowed in inductive definitions. If L is the type of terms of the language being defined, the usual way to express the higher-order syntax of an abstraction operator such as function abstraction in our example is to introduce a constant such as Lam and assign it the type (L -> L) -> L. That is, Lam takes one argument of functional type. Thus function abstraction in the object-language is expressed using λ-abstraction in the meta-language. As a result, bound variables in the object-language are identified with bound variables in the meta-language. In inductive types in Coq, negative occurrences such as the first occurrence of L in the above type are disallowed. As in [3], we get around this problem by introducing a separate type var for variables and giving Lam the type (var -> L) -> L. We must then add a constructor for injecting variables into terms of L. Thus, in our restricted form of higher-order syntax, we still define function abstraction using λ-abstraction in Coq and it is still the case that a-convertible terms in our object-language map to α-convertible terms in Coq, but we cannot directly define object-level substitution using Coq's β-reduction. Instead we define substitution as an inductive predicate. Its definition is simple and similar to the one found in [12].

Is there no way to define object-level substitution using Coq's β?

I think this is the latest incarnation of Felty et al.'s regular HOAS: https://www.site.uottawa.ca/~afelty/HybridCoq/

No, it is not possible. Your original `LC`

type is trivially inconsistent, by cardinality. But, (P)HOAS comes quite close to functions and substitution. Instead of writing `Abs (\x -> App x x)`

, you write `Abs (\x -> App (Var x) (Var x))`

.

Ah! I didn't know that Coq's types weren't just computable sets, all of which necessarily have countable cardinality. OK, I can see now why that wouldn't work. Thanks.

@Karl Palmskog Thanks, I'll have a look.

They're countable from the *outside* :)

Last updated: Oct 13 2024 at 01:02 UTC