Именованная реализация к реализации по умолчанию

Question

Я определил именованную реализацию для класса типов Ord для типа Int.

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

Возможно ли это в Идрисе?

Answer 1

Это возможно, поскольку Idris 0.12 использует using-блоков:

Экспортируйте ваш названный интерфейс в один модуль, скажем 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],