在构造数据类型时选择类型类

Question

我在 idris 中有一个数据类型：

data L3 = Rejected | Unproven | Proven

我验证了它是一个具有单位、格、群和其他一些属性的环。

现在我想创建一个对象，它保留了我注入其中的语句的表达式。我从四个类别开始来表示所有操作，因此我从中得到了一个很好的语法树。例如：

Om [Proven, Unproven, Op [Proven, Oj [Unproven, Proven]]

这不是真正的表示，我去掉了一些需要的难看的部分，但它给出了我试图实现的想法，上面相当于：

meet Proven (meet Unproven (Proven <+> (join Unproven Proven)))

我意识到我可以将这些数据类型合并为一个。为此，我创建了一个函数，它将选择正确的 class 实例：

%case data Operator = Join | Meet | Plus | Mult

classChoice : (x: Operator) -> (Type -> Type)
classChoice Join = VerifiedJoinSemilattice
classChoice Meet = VerifiedMeetSemilattice
classChoice Plus = VerifiedGroup
classChoice Mult = VerifiedRing

所以我可以保证类型中的任何内容都代表这四种操作之一：

 %elim data LogicSyntacticalCategory : classChoice op a => (op : Operator) -> (a : Type) -> Type where
       LSCEmpty : LogicSyntacticalCategory op a

它会抱怨：

When elaborating type of logicCategory.LSCEmpty:
Can't resolve type class classChoice op ty

现在我的问题是：如何确保我的数据类型中的对象经过验证并将四种不同的数据类型合并为一种。我真的很想确保在施工期间这是真的。我可以理解现在解析类型 class 有困难，但我希望 Idris 确保它可以在稍后的构建过程中完成。我怎样才能做到这一点？

代码不是真的需要，我很满意一个思路。

Answer 1

先说两个小问题：... -> a -> ...应该是... -> (a : Type) -> ...，句法就是这么写的

警告：我正在使用 Idris 0.9.18，还不知道如何编写 Elab 证明。

存储库：https://github.com/runKleisli/idris-classdata

在具有这些相同类型签名的普通函数中，您有机会在定义函数时通过策略协助类型 class 解析。但是对于数据类型及其构造函数，你只有声明它们的机会，所以你没有这样的机会来协助解析。看来这里需要这样的指导性解决方案。

看来classChoice op a需要一个实例证明在LSCEmpty定义中的LogicSyntacticleCategory op a有意义之前，它没有得到这个实例。 Class 像这样的数据类型类型的约束通常会自动引入构造函数的上下文中，就像隐式参数一样，但这似乎在这里失败了，并且假设一个实例的类型与所需的类型不同.为构造函数假设的实例不满足通过声明 LogicSyntacticleCategory op a 引入的目标似乎是错误。在存储库中的一个示例中，这些意外不匹配的目标和假设似乎能够自动配对，但不是在数据类型和构造函数声明的情况下。我无法找出确切的问题，但它似乎不适用于在类型签名上具有相同条件的普通函数声明。

存储库中给出了几个解决方案，但最简单的一个是替换约束参数，说需要 classChoice op a 的实例，具有类型 classChoice op a 的隐式参数，并且评估 LogicSyntacticleCategory 喜欢

feat : Type
feat = ?feat'

feat' = proof
  exact (LogicSyntacticleCategory Mult ZZ {P=%instance})

如果您在数据类型的主接口中设置了约束参数，则可以将 LogicSyntacticleCategory : (op : Operator) -> (a : Type) -> {p : classChoice op a} -> Type 的定义包装在函数

中

logicSyntacticleCategory : classChoice op a => (op : Operator) -> (a : Type) -> Type
logicSyntacticleCategory = ?mkLogical

mkLogical = proof
    intros
    exact (LogicSyntacticleCategory op a {P=constrarg})

当你想创建一个 LogicSyntacticleCategory op a 形式的类型时，像以前一样计算，但是

feat' = proof
  exact (logicSyntacticleCategory Mult ZZ)
  exact Mult
  exact ZZ
  compute
  exact inst -- for the named instance (inst) of (classChoice Mult ZZ)

匿名实例的最后一行被删除。

在构造数据类型时选择类型类

Choosing a typeclass on construction of a data type

dependent-type

idris