Drawing arrows and coding functions $\blacktriangleright$ A type system as a model for some concepts $\blacktriangleright$ Foundational temp1 |
We introduce some basic notions of Idris, namely those that can be seen as “semantics” for logic, set theory and category theory (or rather topoi, as discussed in Leinster, Rethinking set theory). However, we always treat the (chosen subpart of the) language from a syntactical perspective as a programming language, as is, and don't “force it into” a known mathematical structure. In particular, many forms of “equality” often make problems. Then again, it's always good to know how to map your stuff into mathematical frameworks (e.g. into a well defined category), even if that mapping is neither surjective nor even injective.
(161013 The code presented below is also all included on the page Idris syntax, but that's just for now.)
Want to talk about functions, need types
Beagle, Kid
Draw the corresponding arrows (akin to Lawyeres babby book)
For any number {0, 1, 2, 3, …, 17, 18, …} we can form a type with that many terms
basic function definition (forth, back, permutation, identity)
Draw the corresponding arrows (akin to Lawyeres babby book)
given $f:X\to Y$, point out how $i:S\to{X}$ and $j:X\to{T}$ induces functions $(f\circ{i}):S\to Y$, $(j\circ{f}):X\to T$ with potentially restricted domain resp. codomain. It's always interesting to see how a given function $g$ may factor into other functions. Parts of “factors” may be general and important functions, defined for very general input, or e.g. components of natural transformations, etc.
data Pullback : (f : x -> z) -> (g : y -> z) -> Type where MkPullback : (tx : x) -> (ty : y) -> (f tx = g ty) -> (Pullback f g) -- MkPullback maps a term tx, a term ty and a proof -- that f tx = g ty to a global element of Pullback f g times8 : Nat -> Nat times8 k = k*8 square : Nat -> Nat square n = n*n aSolution : Pullback Test.times8 Test.square aSolution = MkPullback 2 4 Refl -- The compiler already reduces the type '2*8 = 4*4' to '16 = 16' and Refl proves this --willNotCompile : Pullback Test.times8 Test.square --willNotCompile = MkPullback 3 5 Refl -- The compiler reduces '3*8 = 5*5' to '24 = 25' and then down to '0 = 1' -- but there is actually no way to prove this. In particular, Refl won't do
cheap product
actual product syntax
(infinitely large type)
using dependent types, prove the properties discussed below (if possible)
identity exists
associations
of empty
of unit
of product
of exponential object
of Nat
all of the above in terms of universal properties
Type level functions (type constructors)
Functors
Monads