デフォルト実装への名前付き実装

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

これはusing -blocks使用イドリス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] 

これはを印刷する必要があります。