git.iko.soy/Idris-dev
on ee8fce0 help sign in
Idris-dev/test/basic012/basic012.idr
62 lines 1.3 kB history raw
1import Data.Vect
2import Control.Monad.State
3import Control.Monad.Identity
4
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
34foost: AnyST Int ()
35foost = do x <- get
36 put x
38wibble : StateT Int Maybe ()
39wibble = foost
41appShow : Show a => ({b : _} -> Show b => b -> String) -> a -> String
42appShow s x = s x
44myshow : Show a => a -> String
45myshow = show
47baz : Int -> String
48baz x = appShow myshow x ++ appShow show x
50tupleId : ({a : _} -> a -> a) -> (a, b) -> (a, b)
51tupleId f (a, b) = (f a, f b)
53AppendType : Type
54AppendType = {a, n, m : _} -> Vect n a -> Vect m a -> Vect (n + m) a
56append : AppendType
57append [] ys = ys
58append (x :: xs) ys = x :: append xs ys
60main : IO ()
61main = do putStrLn (baz 42)
62 print (append [1,2,3] [4,5,6])