Qazrw70uukxtafyahte0
SkillsCast

Lightning Talk: Protop--Dependent Types through Topoi

12th October 2017 in London at CodeNode

There are 36 other SkillsCasts available from Haskell eXchange 2017

Please log in to watch this conference skillscast.

661993685 640

The idea of this talk is to take a somewhat unusual route to dependent types, not via type-theory, but rather by trying to model a "topos" in Haskell. A "topos" is a special kind of category which is basically a theory of sets that makes it possible to do most of the usual constructions from set theory. In particular, one gets quotient types, subtypes, extensional equality for functions etc. The "protop" library models such (elementary) topoi in Haskell and can compile topos objects to Haskell types and topos morphisms to Haskell functions.

YOU MAY ALSO LIKE:

Thanks to our sponsors

Lightning Talk: Protop--Dependent Types through Topoi

Lars Brünjes

Lars is a pure mathematician by training, and holds a PhD in the same. He has spent several years teaching and doing postgraduate research in arithmetic number theory at Cambridge University in the UK, and at Regensburg University in Germany. He worked for ten years as a Lead Software Architect for an international IT company. His job, amongst other things, was the application of mathematical optimization techniques to the paper industry and web framework development (using mostly C#, JavaScript and TypeScript). His present position is that of Director of Education at Input Output Hong Kong (IOHK), working on blockchain technology and teaching Haskell and other subjects. He has been interested in programming since his early teens, and he loves learning new programming languages and paradigms - in particular those that offer a radically new way of looking at problems and of thinking about solutions. He is especially fascinated by functional programming and its promise of elegant, bug-free code that can be developed rapidly.

SkillsCast

Please log in to watch this conference skillscast.

661993685 640

The idea of this talk is to take a somewhat unusual route to dependent types, not via type-theory, but rather by trying to model a "topos" in Haskell. A "topos" is a special kind of category which is basically a theory of sets that makes it possible to do most of the usual constructions from set theory. In particular, one gets quotient types, subtypes, extensional equality for functions etc. The "protop" library models such (elementary) topoi in Haskell and can compile topos objects to Haskell types and topos morphisms to Haskell functions.

YOU MAY ALSO LIKE:

Thanks to our sponsors

About the Speaker

Lightning Talk: Protop--Dependent Types through Topoi

Lars Brünjes

Lars is a pure mathematician by training, and holds a PhD in the same. He has spent several years teaching and doing postgraduate research in arithmetic number theory at Cambridge University in the UK, and at Regensburg University in Germany. He worked for ten years as a Lead Software Architect for an international IT company. His job, amongst other things, was the application of mathematical optimization techniques to the paper industry and web framework development (using mostly C#, JavaScript and TypeScript). His present position is that of Director of Education at Input Output Hong Kong (IOHK), working on blockchain technology and teaching Haskell and other subjects. He has been interested in programming since his early teens, and he loves learning new programming languages and paradigms - in particular those that offer a radically new way of looking at problems and of thinking about solutions. He is especially fascinated by functional programming and its promise of elegant, bug-free code that can be developed rapidly.

Photos