This is an old revision of the document!


A type system as a model for some concepts

Drawing arrows and coding functions $\blacktriangleright$ A type system as a model for some concepts $\blacktriangleright$ Foundational temp1

Guide

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.)

(161013 The code presented below is also all included on the page Idris syntax, but that's just for now.)

tmp Overview

easy
  • 2 There is a set {0} with exactly one element
  • 3 There is a set {} with no elements
  • 6 Given sets X and Y, one can form the set of functions from X to Y
  • 5 Given sets X and Y, one can form their Cartesian product X x Y (pullback with {0} in the middle)
  • 9 The natural numbers form a set
  • 1 Composition of functions is associative and there are identity functions
harder (needs dependent types)
  • 8 The subsets of a set X correspond to the functions from X to {0,1} (subobject classifier pullback)
  • 7 Given f:X→Y and y:Y, one can form the inverse image of f (pullback with {0} on one side)
harder (ew)
  • 10 Every surjection has a right inverse (muh axiom of choice, easy if surjective functions are defined as function type where surjectivity must be proven for terms)
  • 4 A function is determined by its effect on elements (muh (function) extensionality)

Types

Want to talk about functions, need types
Finite 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
Unit type
Empty type

Functions

Function type
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.
introduce dependent types
Pullback
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

Product
cheap product
actual product syntax
injections, subsets
Nats

(infinitely large type)

Properties

using dependent types, prove the properties discussed below (if possible)

of Functions
identity exists
associations
of Types
of empty
of unit
of product
of exponential object
of Nat
caty
all of the above in terms of universal properties

More on Functions

Type level functions (type constructors)
Functors
Monads

Reference

Sequel of

Link to graph
Log In
Improvements of the human condition