Skip to content

Latest commit

 

History

History
30 lines (20 loc) · 887 Bytes

overview.md

File metadata and controls

30 lines (20 loc) · 887 Bytes
Raw

Overview

Contents

  • Getting started with Idris
  • An introduction to type-driven development
  • The essence of pure functional programming

Notes

  • Type-driven development:

    1. Write a Type to represent the system we are modelling
    2. Define a function over that type
    3. Refine the type and definition as necessary to capture any missing properties, or to help ensure totality

  • two distinct features:

    • In Idris, types are a first-class language construct. A first-class language construct is one for which there are no syntactic restrictions on where or how it can be used.
    • Idris functions themselves can contain holes. A function with a hole is incomplete. Only a value of an appropriate type will fit into the hole.

  • Type has type Type 1, then Type 1 has type Type 2, and so on.

Exericises

1.3.4 Introductory Exercises

  1. id
  2. append
  3. tail
  4. index