User Defined Types
A user defined type is constructed using the 'data' keyword.
The simplest form just lists the constructors.
data PrimaryColour = Red | Green | Blue |
These type constructors can have parameters:
data Point2D = Pt Double Double |
We can also use 'where' syntax:
data Point2D : Type where Pt : Double -> Double -> Point2D |
If we want to define Point types in 3 or more dimensions then, we could either repeat the definition
data Point : Nat ->Type where Nil : Point Z (::) : Double -> Point k -> Point (S k) |
So, in the first case the type would just be referred to by name 'Point2D' in the second case the type name must always include a number 'Point 2'.
'Point', on its own is not a type, it might be known as a 'type constructor'.
Generic Data Types
A type that's parameterised over some other type (type depends on type).
Type is represented by variable name starting with lower case.
data Maybe valtype = Nothing | Just valtype |
Idris Polymorphism
Implemented by interface.
This is a type spec which must be implemented by implementations of the interface.
| Example Eq |  |
| A specific implementation: | Eq Colour where Red Red = True Blue Blue = True Green Green = True _ _ = False |
Use
x==Red
(pattern match)
Parametric Polymorphism
Example: Functor
'Theorems for free' Reynolds abstraction Theorm
With Block
