CODEWITHSUNDEEP
typeclassidris
Cedric Berlanger
Cedric Berlanger

Reputation: 63

named implementation to default implementation

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"

--

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?

Upvotes: 4

Views: 158

Answers (1)

Julian Kniephoff
Julian Kniephoff

Reputation: 1023

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

Upvotes: 4

Related Questions