Introduction to Dependent Types with Idris: Encoding Program Proofs in Types

© The Author(s), under exclusive license to APress Media, LLC, part of Springer Nature 2023

B. SitnikovskiIntroduction to Dependent Types with Idrishttps://doi.org/10.1007/978-1-4842-9259-4_4

4. Programming in Idris

Boro Sitnikovski¹  

(1)

Skopje, North Macedonia

 

This chapter introduces the Idris syntax and then defines its functions and types.

Depending on the level of abstraction you are working on, types and proofs can give you a kind of security based on some truths you take for granted (axioms). In fact, this is how you develop code on a daily basis, as a software engineer. You have a list of axioms, for example, a foreach loop in a programming language, and build abstractions from it, expecting the foreach to behave in a certain way. However, ...