Name: Dependent Types in Haskell: Binomial Heaps
Start: 2018-12-18T19:00:00+01:00
End: 2018-12-18T21:00:00+01:00
Location: Bedrijfscentrum De Punt

Jasper Van der Jeugt: Dependent Types in Haskell: Binomial Heaps

Most people are familiar with the hello world of dependently-typed Haskell: a vector that is annotated with the Peano number represenation of its size. This talk introduces a similar way to deal with binomial heaps.

Binomial heaps are used to implement, among other things, priority queues. They are a fan favourite among data structures because of their simple elegance and the fascinating way their structure corresponds to binary numbers.

Jasper will use this idea to lift binary numbers to the type level, which is great because you get `log(n)` size and time in places where you would see `n` for Peano numbers -- in addition to being insanely cool.

This talk will be an introductory explanation of a non-trivial example of dependent Haskell programming.

Koen De Keyser

Mark Christiaens

Ghent Functional Programming Group Meetup

Technology

Functional Programming

Software Development

Haskell

Computer Programming

Programming Languages

Dependent Types in Haskell: Binomial Heaps

Bedrijfscentrum De Punt

Share

Ghent Functional Programming Group Meetup

Dependent Types in Haskell: Binomial Heaps

Ghent Functional Programming Group Meetup

Details

Members are also interested in