Last active
December 29, 2018 09:47
-
-
Save CarstenKoenig/361a138af77ef1ac340b239162070589 to your computer and use it in GitHub Desktop.
dep. arity sum function in idris
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
notice how you can write a function that depends on values and produces a type (
codom
anddepType)? this function can then be used in signatures (see
strangeFun,
sumAccand
sumN`)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!