Thorsten started by talking about Ask: a total fragment of Haskell. Key features include:
- Ask distinguishes between data and codata.
- Ask incorporates some kind of first-order predicate logic.
- Ask has both quotient types and subtypes
Thorsten would like to use Ask as a pedagogical tool. You can reason about Ask programs very nicely. For example, you could use Ask to construct a pure model of I/O fuctions.
Conor would like to use Ask to justify what is happening in Haskell’s type system and introduce something a bit like dependent types. Conor speculated how one could allow constructor patterns to appear freely within types. Having a total fragment of your language is very important here – otherwise you lose all hope of having a somewhat sane type system. I’m paraphrasing a lively discussion, so forgive me if I got something wrong.
Afterwards, I talked a bit about arrows and stream processors. Thorsten and I claim that John Hughes’s example of stream processors as arrows are not really arrows. There are two alternative definitions of composition, both which fail to satisfy all the arrow laws. The definition of first and the laws that it must satisfy is where most of the problems are. On the other hand, the stream processors do carry a coproduct structure. We speculated how we could then generalize the definition of arrow to allow other monoidal structures.