For anyone interested in AGDA, I found this [0] paper really helpful for getting my head around dependent typing. I sort of doubt that dependently typed languag

For anyone interested in AGDA, I found this [0] paper really helpful for getting my head around dependent typing. I sort of doubt that dependently typed languages are ever going to catch on, but they embody some seriously cool ideas about how to verify program correctness. Also, AGDA has probably the most flexible syntax for defining function fixiness, letting you easily define new "syntax": if_then_else_ : {A : Set} -> Bool -> A -> A -> A if true then x else y = x if false then x else y = y [0] http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf