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 , 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 .
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: Feb 01 2023 at 11:04 UTC