typeclass - 命名实现为默认实现

我为类型Ind的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]

伊德里斯有可能吗？

最佳答案

这是可能的，因为使用using块的Idris 0.12：

将命名接口导出到一个模块中，例如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块中，如下所示：

-- 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]。