add a tutorial for polarity for haskellers

[MangoIV]

I was writing this down yesterday while I thought a bit about how to compile polarity (the non-dependent fraction)

rendered

[codecov]

Codecov Report

All modified and coverable lines are covered by tests ✅

see 25 files with indirect coverage changes

[BinderDavid]

Super cool! I will go through and add some nitpicks. This also reminds me of https://inria.hal.science/hal-01653261/document by Laforgue and Regis-Gianas, who showed how to encode codata types in OCaml (instead of using Strict Haskell).

[timsueberkrueb]

Very cool, I'm wondering whether we could put this on the website instead, where it might be more accessible? Maybe we could have a section with guides/tutorials. Just an idea, happy to discuss :)

[timsueberkrueb]

Some spelling mistakes.

[timsueberkrueb]

Also in this context, we should perhaps note why we model infinite objects using codata and not via lazy data types with constructors. I think the issue is best explained by Berger and Setzer. They showed that pattern matching on streams defined by constructors is not a valid principle: there exists no decidable equality for streams which admits one step expansion s.t. any stream 𝑠 is equal to (cons n s) for some n, s. Originally these issues were found by Giménez and later rediscovered in Coq when subject reduction broke.

[timsueberkrueb]

One more note: The title is "Polarity for Haskellers" but at the moment it solely focuses on how to model infinite objects in Haskell vs Polarity. There are other differences worth mentioning, such as Polarity not having a built-in function type. So maybe we should change the title to "Codata for Haskellers" or expand on some of these other aspects?

Let's wait for @BinderDavid's thoughts on this.

[MangoIV]

One more note: The title is "Polarity for Haskellers" but at the moment it solely focuses on how to model infinite objects in Haskell vs Polarity. There are other differences worth mentioning, such as Polarity not having a built-in function type. So maybe we should change the title to "Codata for Haskellers" or expand on some of these other aspects?

No you are completely right. I should also write about this or at least make it more clear how haskell functions relate to the codata types of polarity.