我可以在Idris中定义x==y = p(x) == p(y)的一般概念吗？
我可以在Idris中定义x==y = p(x) == p(y)的一般概念吗？
提问于 2017-05-15 16:58:21
我想定义一个类型构造函数，它体现了使用类型包装器在域类型t1上定义相等的概念，方法是使用函数p投影到域类型t2上。
以下特定示例有效，其中t1 = ABC，t2 = Nat，p是函数abc_2_nat
%default total
data ABC = A | B | C
abc_2_nat : ABC -> Nat
abc_2_nat A = 1
abc_2_nat B = 1
abc_2_nat C = 2
data Projected_abc : Type where
Project_abc : ABC -> Projected_abc
Projected_abc_equals : Projected_abc -> Projected_abc -> Bool
Projected_abc_equals (Project_abc x) (Project_abc y) = abc_2_nat x == abc_2_nat y
Eq Projected_abc where
(==) = Projected_abc_equals但是，当我尝试概括如下时：
data Projected : t1 -> t2 -> (p: t1 -> t2) -> Type
where Project : t1 -> Projected t1 t2 p
Projected_equals : Projected t1 t2 p -> Projected t1 t2 p -> Bool
Projected_equals (Project x) (Project y) = ?hole我得到了这个洞：
- + Main.hole [P]
`-- phTy : Type
t2 : phTy
p : Type -> phTy
t1 : Type
x : t1
y : t1
--------------------------
Main.hole : Bool这不起作用，因为它没有识别出p是t1->t2类型(这正是我想要的)。
我怀疑我要求将投影函数作为参数提供给类型构造函数，并且以某种方式使投影函数在其参数属于构造类型的函数的定义范围内可用。
有什么方法可以让它工作吗？
回答 1
Stack Overflow用户
发布于 2017-05-15 17:32:57
这是可以做到的。您的Projected泛化还不够准确。您应该指定t1和t2的类型。如下所示：
data Projected : (t1: Type) -> (t2: Type) -> (p: t1 -> t2) -> Type where
Project : t1 -> Projected t1 t2 p没有这个Idris编译器就无法猜测t1和t2到底是什么类型的东西。另请注意:要通过将projections与t2域进行比较来比较t1类型的值，应该确保可以比较t2类型的值。因此，一般的投影等式如下所示：
projected_equals : Eq t2 => Projected t1 t2 p -> Projected t1 t2 p -> Bool
projected_equals {p} (Project x) (Project y) = p x == p y你可以为它编写Eq实例！
Eq t2 => Eq (Projected t1 t2 p) where
(==) = projected_equals而且它也是有效的。所以如果你这样定义的话：
data ABC = A | B | C
abc_2_nat : ABC -> Nat
abc_2_nat A = 1
abc_2_nat B = 1
abc_2_nat C = 2您可以使用您的abc_2_nat投影来实现相应的投影仪：
abcNatProjector : ABC -> Projected ABC Nat Main.abc_2_nat
abcNatProjector abc = Project abc我必须使用Main.abc_2_nat来解决多义性，因为否则abc_2_nat可以是任何隐式类型参数。Idris没有能力猜测你想要什么。很高兴，编译器帮助我解决了这个警告：
Eq.idr:13:37-46:WARNING: abc_2_nat is bound as an implicit
Did you mean to refer to Main.abc_2_nat?现在你可以在REPL中检查它是否正常工作！
λΠ> abcNatProjector A == abcNatProjector B
True : Bool
λΠ> abcNatProjector A == abcNatProjector C
False : Bool额外奖励：
如果将abcNatProjector标记为implicit函数，如下所示：
implicit
abcNatProjector : ABC -> Projected ABC Nat Main.abc_2_nat
abcNatProjector abc = Project abc你可以定义一些花哨的运算符
infixr 5 ==^
(==^) : Eq t2 => Projected t1 t2 p -> Projected t1 t2 p -> Bool
(==^) = projected_equals并在不显式使用abcNatProjector的情况下将ABC类型的值与它进行比较。
λΠ> A ==^ B
True : Bool
λΠ> A ==^ C
False : Bool页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/43975230
复制相关文章
相似问题
腾讯云开发者
