3

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

data L3 = Rejected | Unproven | Proven

我证实它是一个具有统一性、格子、组和其他一些属性的环。

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

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 确保它可以在构建过程中稍后完成。我怎样才能做到这一点？

代码并不是真正需要的，我对思想方向感到非常满意。

4

1 回答 1

3

首先是两个小问题：... -> a -> ...应该是... -> (a : Type) -> ...，语法是它的编写方式。

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

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

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

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

存储库中给出了几个解决方案，但最简单的一个是用classChoice op atype 的隐式参数替换约束参数，说需要一个实例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)

对于匿名实例，最后一行被删除。

于 2016-02-21T18:37:04.740 回答