dep. arity sum function in idris

DepSum.idr

module SimpleDep

basic : (b : Bool) -> if b then String else Int
basic True = "it's true"
basic False = 0

-------------

data WhatIsIt = AString | AInt

depType : WhatIsIt -> Type
depType AString = String
depType AInt    = Int


strangeFun : (w : WhatIsIt) -> depType w
strangeFun AString = "Hello"
strangeFun AInt = 5


-------

codom : Nat -> Type
codom Z = Int
codom (S n) = Int -> codom n


sumAcc : (n : Nat) -> Int -> codom n
sumAcc  Z     acc = acc
sumAcc  (S k) acc = \ x => sumAcc k (acc + x)


sumN : (n : Nat) -> codom n
sumN n = sumAcc n 0


eleven : Int
eleven = sumN 2 5 6

add10 : Int -> Int
add10 = sumN 2 10


add3Numbers : Int -> Int -> Int -> Int
add3Numbers = sumN 3

notice how you can write a function that depends on values and produces a type (codom and depType)? this function can then be used in signatures (see strangeFun, sumAccandsumN`)

so you can have really strange things like strangeFun that's result type depends on the input but is actually type-checked!

also you can have variable arity functions like sumN

in a sense you can get many things thought only possible in dynamic languages but with guarantees and that is only the beginning - this path soon leads into a place where you are proofing theorems by writing functions etc. ... highly recommended topic!