- Functions in Idris are defined by collections of pattern-matching equations.
- Patterns arise from the constructors of a data type.
- Describe "type declaration", "type definition", "equation", "expression"
- Are type declarations required? When (not)?
- What is referential transparency?
- Can pattern matching match a specific value?
- How would you recurse from 0 to n?
- The Atom text editor provides an interactive editing mode that uses the type to help direct function implementation. Similar modes are available for Emacs and Vim.
- Interactive editing commands provide natural tools for following the process of type, define, refine.
- Interactive editing provides a command for searching for a valid expression that satisfies the type of a hole.
- What are the interactive editor commands that support type, define, refine?
- More-precise types, such as Vect, give more information to the compiler both to help check that a function is correct, and to help constrain expression searches.
- Matrices are two-dimensional vectors, with the dimensions encoded in the type. Operations on matrices such as addition and multiplication can be given types that precisely describe how the operations affect the dimensions.
- What are type-level variables?
- What other type-level constructs do you imagine might exist?
- The type-define-refine process helps you to implement matrix operations with precise types by using the type to direct the implementation of each subexpression and create appropriate helper functions.
- Type-level variables are implicit arguments to functions, which can be brought into scope and used like any other arguments by enclosing them in braces {}.
- Why would you want to bring implicit arguments into scope explicitly?
Given a square matrix, calculate the absolute difference between the sums of its diagonals.
3
11 2 4
4 5 6
10 8 -12
15
- Data types are defined in terms of a type constructor and data constructors.
- What is the difference between a 'type constructor' and a 'data constructor'?
- Enumeration types are defined by listing the data constructors of the type.
- Union types are defined by listing the data constructors of the type, each of which may carry additional information.
- Generic types are parameterized over some other type. In a generic type definition, variables stand in place of concrete types.
- Dependent types can be indexed over any other value.
- What does it mean for a type to be 'indexed' over any other value?
- Using dependent types, you can classify a larger family of types (such as vehicles) into smaller subgroups (such as vehicles powered by petrol and those powered by pedal) in the same declaration.
- What is a 'type family'?
- Dependent types allow safety checks to be guaranteed at compile time, such as guaranteeing that all vector accesses are within the bounds of the vector.
- You can write larger programs in the type-driven style, creating new data types where appropriate to help describe components of the system.
- Interactive programs that involve state can be written using the
replWithfunction.
Discuss Interface Patterns
N/A
N/A
- Idris provides a generic IO type for describing interactive actions.
- Idris distinguishes between evaluation of pure functions and execution of interactive actions. The :exec command at the REPL executes interactive actions.
- You can sequence interactive actions using do notation, which translates to applications of the >>= operator.
- You can produce pure values from interactive definitions by using the pure function.
- Idris provides a concise notation for pattern-matching on the result of an interactive action.
- Dependent types express assumptions about inputs to functions, so you need to validate user inputs to check that they satisfy those assumptions.
- Dependent pairs allow you to pair two values, where the type of the second value is computed from the first value.
- You can use dependent pairs to express that a type’s argument, such as the length of a vector, will not be known until the user enters some input.
- What other uses of dependent pairs can you think of?
- See Monads
- Implement the IO monad (hint)
- Type synonyms are alternative names for existing types, which allow you to give more-descriptive names to types.
- Type-level functions are functions that can be used anywhere that Idris is expecting a Type. Type synonyms are a special case of type-level functions.
- Type-level functions can be used to compute types, and they allow you to write functions with varying numbers of arguments, such as printf.
- You can represent a schema for a data store as a type, and then use type-level functions to calculate the types of operations, such as parsing and displaying entries in the data store from the schema description.
- A record is a data type with only one constructor, and with automatically generated functions for projecting fields from the record.
- After refining a data type, you can use holes to correct compilation errors temporarily.
- Using do notation, you can sequence computations that use Maybe to capture the possibility of errors.
Implement scanf to mirror printf.