dependent-type - 在构造数据类型时选择类型类

Question

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

data L3 = Rejected | Unproven | Proven

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

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

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

这不是真正的表示，我去掉了一些需要的丑陋部分，但它给出了我试图实现的目标的想法，上面等同于:

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

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

%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

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

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

Answer 1

首先是两个小问题:... -> a -> ... 应该是 ... -> (a : Type) -> ... , 句法就是它的书写方式。

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

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

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

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

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

feat : Type
feat = ?feat'

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

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

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)

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