Idris - 派生扩展接口实例答案

【问题标题】：Idris - derive extended interface instanceIdris - 派生扩展接口实例
【发布时间】：2019-02-23 11:34:32
【问题描述】：

假设我有一个函数f : Ord a => ...，它需要a 和Ord 实例。我可以使用

访问Ord a实例

f : Ord a => ...
f @{ord} ...

由于Eq a => Ord a，a 还需要有一个Eq a 实例。有没有办法直接从Ord a 检索它，而不是像下面这样？

f : (Eq a, Ord a) => ...
f @{eq} @{ord} ...

【问题讨论】：

【解决方案1】：

可以使用%implementation，做如下操作：

eqFromOrd : Ord a => Eq a
eqFromOrd @{ord} = %implementation

【讨论】：

【解决方案2】：

我会使用@marcosh 的解决方案，但这里有另一种看法，表明我们并不严格需要%implementation：

eqExplicit : Eq a => Eq a
eqExplicit @{eq} = eq

eqFromOrd : Ord a => Eq a
eqFromOrd = eqExplicit

【讨论】：