- Enumerated types—Types defined by giving the possible values directly
- Union types—Enumerated types that carry additional data with each value
data Shape = Triangle Double Double | Rectangle Double Double | Circle Double
- Recursive types—Union types that are defined in terms of themselves
- Generic types—Types that are parameterized over some other types
data Either a b = Left a | Right b
data Maybe val = Nothing | Just val
- Dependent types—Types that are computed from some other value.
Vect : Nat -> Type -> Type : The type depends on its length
anyVect : (n ** Vect n String). The function is created kind of ad hoc once the data comes in, rather than beforehand.
span finds the first space in an input
unpack : String -> List Char converts a String into a list of characters.
isDigit : Char -> Bool returns whether a Char is one of the digits 0–9.
all : (a -> Bool) -> List a -> Bool returns whether every entry in a list satisfies a test.
cast : cast operation? change type from one to another
pure : IO wrapper for value
printLin : Show a => a -> IO () displays value at console directly
- While everything is brought together in
main, the program is started by calling
:exec from the repl, not
- IO is an interactive program that returns a description of an IO action. Think recipe rather than execution
- Sometimes you need to pass result of executed function in the repl with
- Functions can be chained in the repl with bind i.e.
:exec readVect >>= printVect