import Data.Vect
import Control.Monad.State
import Control.Monad.Identity

VThing : Type
VThing = {n : Nat} -> Vect n Int -> Int

foo : Int -> Vect m Int -> ({n : Nat} -> Vect n Int -> Int) -> Int
foo x xs f = x + f xs

foo' : Int -> Vect m Int -> VThing -> Int
foo' x xs f = x + f xs

bar : Int -> VThing
bar y [] = 0
bar y (x :: xs) = y + x + bar y xs

vsum : Vect n Int -> Int
vsum [] = 0
vsum (x :: xs) = x + vsum xs

testfoo : Vect n Int -> Int
testfoo xs = foo 42 xs (\ xs => vsum xs)

testfoo2 : Vect n Int -> Int
testfoo2 xs = foo' 42 xs vsum

testfoo3 : Vect n Int -> Int
testfoo3 xs = foo 42 xs (bar 10)

AnyST : Type -> Type -> Type
AnyST s a = {m : _} -> Monad m => StateT s m a

-- foost : AnyST Int ()
foost : StateT Int Maybe ()
foost = do x <- get
           put x

wibble : StateT Int Maybe ()
wibble = foost

appShow : Show a => ({b : _} -> Show b => b -> String) -> a -> String
appShow s x = s x

myshow : Show a => a -> String
myshow = show

baz : Int -> String
baz x = appShow myshow x ++ appShow show x

tupleId : ({a : _} -> a -> a) -> (a, b) -> (a, b)
tupleId f (a, b) = (f a, f b)

AppendType : Type
AppendType = {a, n, m : _} -> Vect n a -> Vect m a -> Vect (n + m) a

append : AppendType
append [] ys = ys
append (x :: xs) ys = x :: append xs ys

main : IO ()
main = do putStrLn (baz 42)
          printLn (append [1,2,3] [4,5,6])