{"guid":"6ad93148-6a8c-4a3e-bd17-f956bdf2295b","title":"Theorems for free","subtitle":null,"slug":"bob2021-theorems-for-free-hupel","link":"https://bobkonf.de/2021/miller.html","description":"\t In the typed functional programming communities, there is\n\t much talk about “reasoning with types”. But rarely is this\n\t elaborated into something concrete. Just how can we extract\n\t tangible information from types beyond playing mere type\n\t tetris? The secret sauce is called parametricity, first\n\t described by John C. Reynolds, and later applied to Haskell\n\t by Philip Wadler in his seminal paper “Theorems for free!”.\n\t\n\n\t","original_language":"eng","persons":["Lars Hupel"],"tags":["bob2021","1","2021","Talk","BOB","BOBKonferenz"],"view_count":82,"promoted":false,"date":"2021-02-26T09:15:00.000+01:00","release_date":"2021-06-19T00:00:00.000+02:00","updated_at":"2026-03-12T20:15:06.075+01:00","length":2175,"duration":2175,"thumb_url":"https://static.media.ccc.de/media/events/bobkonf/2021/1-6ad93148-6a8c-4a3e-bd17-f956bdf2295b.jpg","poster_url":"https://static.media.ccc.de/media/events/bobkonf/2021/1-6ad93148-6a8c-4a3e-bd17-f956bdf2295b_preview.jpg","timeline_url":"https://static.media.ccc.de/media/events/bobkonf/2021/1-6ad93148-6a8c-4a3e-bd17-f956bdf2295b.timeline.jpg","thumbnails_url":"https://static.media.ccc.de/media/events/bobkonf/2021/1-6ad93148-6a8c-4a3e-bd17-f956bdf2295b.thumbnails.vtt","frontend_link":"https://media.ccc.de/v/bob2021-theorems-for-free-hupel","url":"https://api.media.ccc.de/public/events/6ad93148-6a8c-4a3e-bd17-f956bdf2295b","conference_title":"BOB Konferenz 2021","conference_url":"https://api.media.ccc.de/public/conferences/bobkonf2021","related":[],"recordings":[{"size":204,"length":2175,"mime_type":"video/webm","language":"eng","filename":"bob2021-1-eng-Theorems_for_free_webm-hd.webm","state":"new","folder":"webm-hd","high_quality":true,"width":1920,"height":1080,"updated_at":"2021-06-19T21:46:55.675+02:00","recording_url":"https://cdn.media.ccc.de/events/bobkonf/2021/webm-hd/bob2021-1-eng-Theorems_for_free_webm-hd.webm","url":"https://api.media.ccc.de/public/recordings/54111","event_url":"https://api.media.ccc.de/public/events/6ad93148-6a8c-4a3e-bd17-f956bdf2295b","conference_url":"https://api.media.ccc.de/public/conferences/bobkonf2021"},{"size":54,"length":2175,"mime_type":"video/mp4","language":"eng","filename":"bob2021-1-eng-Theorems_for_free_sd.mp4","state":"new","folder":"h264-sd","high_quality":false,"width":720,"height":576,"updated_at":"2021-06-19T21:46:33.445+02:00","recording_url":"https://cdn.media.ccc.de/events/bobkonf/2021/h264-sd/bob2021-1-eng-Theorems_for_free_sd.mp4","url":"https://api.media.ccc.de/public/recordings/54110","event_url":"https://api.media.ccc.de/public/events/6ad93148-6a8c-4a3e-bd17-f956bdf2295b","conference_url":"https://api.media.ccc.de/public/conferences/bobkonf2021"},{"size":22,"length":2174,"mime_type":"audio/opus","language":"eng","filename":"bob2021-1-eng-Theorems_for_free_opus.opus","state":"new","folder":"opus","high_quality":false,"width":0,"height":0,"updated_at":"2021-06-19T21:46:15.102+02:00","recording_url":"https://cdn.media.ccc.de/events/bobkonf/2021/opus/bob2021-1-eng-Theorems_for_free_opus.opus","url":"https://api.media.ccc.de/public/recordings/54109","event_url":"https://api.media.ccc.de/public/events/6ad93148-6a8c-4a3e-bd17-f956bdf2295b","conference_url":"https://api.media.ccc.de/public/conferences/bobkonf2021"},{"size":33,"length":2174,"mime_type":"audio/mpeg","language":"eng","filename":"bob2021-1-eng-Theorems_for_free_mp3.mp3","state":"new","folder":"mp3","high_quality":false,"width":0,"height":0,"updated_at":"2021-06-19T21:45:57.459+02:00","recording_url":"https://cdn.media.ccc.de/events/bobkonf/2021/mp3/bob2021-1-eng-Theorems_for_free_mp3.mp3","url":"https://api.media.ccc.de/public/recordings/54108","event_url":"https://api.media.ccc.de/public/events/6ad93148-6a8c-4a3e-bd17-f956bdf2295b","conference_url":"https://api.media.ccc.de/public/conferences/bobkonf2021"},{"size":77,"length":2175,"mime_type":"video/webm","language":"eng","filename":"bob2021-1-eng-Theorems_for_free_webm-sd.webm","state":"new","folder":"webm-sd","high_quality":false,"width":720,"height":576,"updated_at":"2021-06-19T21:45:41.547+02:00","recording_url":"https://cdn.media.ccc.de/events/bobkonf/2021/webm-sd/bob2021-1-eng-Theorems_for_free_webm-sd.webm","url":"https://api.media.ccc.de/public/recordings/54107","event_url":"https://api.media.ccc.de/public/events/6ad93148-6a8c-4a3e-bd17-f956bdf2295b","conference_url":"https://api.media.ccc.de/public/conferences/bobkonf2021"},{"size":113,"length":2175,"mime_type":"video/mp4","language":"eng","filename":"bob2021-1-eng-Theorems_for_free_hd.mp4","state":"new","folder":"h264-hd","high_quality":true,"width":1920,"height":1080,"updated_at":"2021-06-19T21:45:36.944+02:00","recording_url":"https://cdn.media.ccc.de/events/bobkonf/2021/h264-hd/bob2021-1-eng-Theorems_for_free_hd.mp4","url":"https://api.media.ccc.de/public/recordings/54106","event_url":"https://api.media.ccc.de/public/events/6ad93148-6a8c-4a3e-bd17-f956bdf2295b","conference_url":"https://api.media.ccc.de/public/conferences/bobkonf2021"}]}