命名实现到默认实现

Question

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

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

如何导入这个命名实现并将其用作 "default"

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

--

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:

在一个模块中导出您的命名接口，比如 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].

命名实现到默认实现

named implementation to default implementation

typeclass

idris