named implementation to default implementation

Question

I defined a named implementation for the typeclass Ord for type Int.

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

How can I import this named implementation and use it as "default"

• so in another module I want to import this implementation
• Mark it as default
• And use it as if it was 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]

Is this possible in Idris?

Answer 1

This is possible since Idris 0.12 using using-blocks:

Export your named interface in one module, say 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

Then just import it in another module and wrap everything that should use it as default in a corresponding using-block like so:

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

This should print [3, 2, 1].