git.iko.soy/Idris-dev
on 385dcbf help sign in
Idris-dev/test/interfaces001/InterfaceName.idr
49 lines 1.1 kB history raw
1module InterfaceName
3||| A fancy shower with a constructor
4||| @ a the thing to be shown
5interface MyShow a where
6 ||| Build a MyShow
7 constructor MkMyShow
8 ||| The shower
9 ||| @ x will become a string
10 myShow : (x : a) -> String
12twiceAString : MyShow a => a -> String
13twiceAString x = myShow x ++ myShow x
15implementation MyShow Integer where
16 myShow x = show x
18badShow : MyShow Integer
19badShow = MkMyShow (const "hej")
21test1 : twiceAString 2 = "22"
22test1 = Refl
24test2 : twiceAString @{InterfaceName.badShow} 2 = "hejhej"
25test2 = Refl
28||| Parent interface fun
29interface MyMagma a where
30 constructor MkMyMagma
31 total op : a -> a -> a
33||| Semigroup
34interface MyMagma a => MySemigroup a where
35 constructor MkMySemigroup
36 total isAssoc : (x, y, z : a) -> op x $ op y z = op (op x y) z
38implementation [addition] MyMagma Nat where
39 op = plus
41additionS : MySemigroup Nat
42additionS = MkMySemigroup @{addition} plusAssociative
44doIt : MySemigroup a => a -> List a -> a
45doIt x [] = x
46doIt x (y :: xs) = doIt (x `op` y) xs
48test : Nat
49test = doIt @{additionS} 22 [1,2,3,4]