Mike Stay (Sep 20 2021 at 19:05): Mike Stay (Sep 20 2021 at 19:05):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?
Guillaume Melquiond (Sep 20 2021 at 19:21):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.
Mike Stay (Sep 20 2021 at 19:31):Can you tell me more about the parametric higher-order abstract syntax?
Guillaume Melquiond (Sep 20 2021 at 19:48):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.
Mike Stay (Sep 20 2021 at 19:51):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 β?
Karl Palmskog (Sep 20 2021 at 19:53):I think this is the latest incarnation of Felty et al.'s regular HOAS: https://www.site.uottawa.ca/~afelty/HybridCoq/
Guillaume Melquiond (Sep 20 2021 at 19:55):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)).
Mike Stay (Sep 20 2021 at 20:03):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.
Mike Stay (Sep 20 2021 at 20:04):@Karl Palmskog Thanks, I'll have a look.
Cody Roux (Sep 20 2021 at 21:26):They're countable from the outside :)
Last updated: Sep 30 2023 at 05:01 UTC