typeclass - 命名实现到默认实现

Question

我为 Int 类型的类型类 Ord 定义了一个命名实现。

[mijnOrd] Ord Int where
  compare n1 n2 = ...

如何导入此命名实现并将其用作“默认”

• 所以在另一个模块中我想导入这个实现
• 将其标记为默认
• 并像默认值一样使用它

--

sort [1,5,2] -- output without importing as default: [1,2,5]
sort [1,5,2] -- output with importing as default: [5,2,1]

这在 idris 可能吗？

Answer 1

从 Idris 0.12 开始，使用 using-blocks 就可以实现这一点:

在一个模块中导出您的命名接口(interface)，例如MyOrd.idr:

module MyOrd

-- Reverse order for `Nat`
export
[myOrd] Ord Nat where
  compare Z Z = EQ
  compare Z (S k) = GT
  compare (S k) Z = LT
  compare (S k) (S j) = compare @{myOrd} k j

然后只需将其导入到另一个模块中，并将应将其用作默认值的所有内容包装在相应的 using block 中，如下所示:

-- Main.idr
module Main

import MyOrd

using implementation myOrd
  test : List Nat -> List Nat
  test = sort

main : IO ()
main = putStrLn $ show $ test [3, 1, 2]

这应该打印 [3, 2, 1]。