on 7afa310 help sign in
Idris-dev/samples/named_instance.lidr
36 lines 892 B history raw
1> module MyOrd
3An alternative Ord instance for Nats, with an explicit name "myord"
4for the dictionary:
6> instance [myord] Ord Nat where
7> compare O (S n) = GT
8> compare (S n) O = LT
9> compare O O = EQ
11The @{name} syntax below gives an explicit dictionary for the compare function.
12Here, we're telling it to use the "myord" dictionary. Otherwise, it'd just
13use the default (unnamed) instance. Note that there can only be one unnamed
14instance --- they must not overlap.
16> compare (S x) (S y) = compare @{myord} x y
18> foo : List Nat
19> foo = [1,4,2,8,3,7,5,6]
21Sort foo using the default comparison operator:
23> test1 : List Nat
24> test1 = sort foo
26-- which gives [1,2,3,4,5,6,7,8]
28Sort foo using the alternative instance. No need for 'sortBy' and other
29such functions. Hoorah!
31> test2 : List Nat
32> test2 = sort @{myord} foo
34-- which gives [8,7,6,5,4,3,2,1]