u/rollingstonei3in r/haskell • Recommends
A Functional Programmer's Guide to Homotopy Type Theory
0:00 / 0:00
#homotopytypetheory#typetheory#icfp
3 01 A Functional Programmer's Guide to Homotopy Type Theory
ICFP Video
3.8K subscribers • 33 videos on Hallway
- Recommended by 1 person: 1 in engineering communities.
Advanced. Deep dive for people who know the field.
27K views10 years ago1 recommendation
Computer scienceProgramming languagesComputation and complexityFunctional programming
An introduction to Homotopy Type Theory tailored for functional programmers, exploring its mathematical foundations and implications.
The uploader added no description.Why it's here
1 person recommends thisMoments people linked to
u/AndrasKovacsin r/haskell • Mentions
On “Suggestion: the more experienced Type-Theory wizards could make a HoTT program assuming no mathematical background.”
I'll try to reiterate the practical uses from Dan Licata's ICFP presentation, because I think it's on the right track (if the goal is to sell HoTT to functional programmers), but the execution was still not simple enough for it to be generally accessible.
Suppose we have a mature implementation of type theory with univalence and higher inductive types (HIT). What can we do that is not possible in Agda (or Haskell for that matter)?
First, univalence lets us do the following:
- If we have an isomorphism between `A` and `B` types, that is: a pair of `f` and `g` functions between them such that `f . g = id` and `g . f = id`
- Then from any program whose type mentions `A`, we get (with O(1…
u/gelisamin r/haskell • Mentions
On “Quotient Types for Programmers”
> I think this is an open research question :)
indeed it is.