git.iko.soy/Idris-dev
on bd8ea0a help sign in
Idris-dev/test/basic012/basic012.idr
63 lines 1.4 kB history raw
1import Data.Vect
2import Control.Monad.State
3import Control.Monad.Identity
5VThing : Type
6VThing = {n : Nat} -> Vect n Int -> Int
8foo : Int -> Vect m Int -> ({n : Nat} -> Vect n Int -> Int) -> Int
9foo x xs f = x + f xs
11foo' : Int -> Vect m Int -> VThing -> Int
12foo' x xs f = x + f xs
14bar : Int -> VThing
15bar y [] = 0
16bar y (x :: xs) = y + x + bar y xs
18vsum : Vect n Int -> Int
19vsum [] = 0
20vsum (x :: xs) = x + vsum xs
22testfoo : Vect n Int -> Int
23testfoo xs = foo 42 xs (\ xs => vsum xs)
25testfoo2 : Vect n Int -> Int
26testfoo2 xs = foo' 42 xs vsum
28testfoo3 : Vect n Int -> Int
29testfoo3 xs = foo 42 xs (bar 10)
31AnyST : Type -> Type -> Type
32AnyST s a = {m : _} -> Monad m => StateT s m a
34-- foost : AnyST Int ()
35foost : StateT Int Maybe ()
36foost = do x <- get
37 put x
39wibble : StateT Int Maybe ()
40wibble = foost
42appShow : Show a => ({b : _} -> Show b => b -> String) -> a -> String
43appShow s x = s x
45myshow : Show a => a -> String
46myshow = show
48baz : Int -> String
49baz x = appShow myshow x ++ appShow show x
51tupleId : ({a : _} -> a -> a) -> (a, b) -> (a, b)
52tupleId f (a, b) = (f a, f b)
54AppendType : Type
55AppendType = {a, n, m : _} -> Vect n a -> Vect m a -> Vect (n + m) a
57append : AppendType
58append [] ys = ys
59append (x :: xs) ys = x :: append xs ys
61main : IO ()
62main = do putStrLn (baz 42)
63 printLn (append [1,2,3] [4,5,6])