bradJust started reading Time and Relational Theory by C.J. Date, Hugh Darwen & Nikos A. Lorentzos. I feel fortunate to have spent some time in Haskell and Haskell-like languages, I think it's helping me to grok the definitions for types and relations more easily (already having a mental model for type and data constructors; which so far seems to map to type generators and possible representations with their selectors).
Also they've just been talking about the set operators: union, intersection and difference. I was a little confused by the n-ary definitions at first, why allow for n to be 0?
Then I thought: hey maybe this is 'foldr operator mempty'? (Seems that is what they mean.) In that case there needs to be an empty unit element for relations in the union case ... but what's the unit element in the 'intersection' case?
That got me thinking: haven’t I seen something like this before? Looks like the unit element for intersection might be something like this: https://hackage.haskell.org/package/lattices-2.0.3/docs/src/Algebra.Lattice.html#line-202.
Brendan Zabarauskas@brad For intersection types I'd think that the unit element would be the `Any` type. For unions the unit element would be the `Void`/`Never` type. Are there any parallels to be had with this?
@brendanzab I’ve been wondering if there isn’t a lot of overlap with row-types. But the intersection here isn’t the intersection of the row-types themselves but two sets containing values of the same row-type… I think relations are a lot like ‘Set r’ where r is some row type.
@brad Ahh ok. Might have to see some more concrete examples to get my head around the relation stuff. I do know you can define records using: the unit type, single element records, and intersection. Is that a similar thing?
@brad Here is an example of using “dependent intersection” for defining dependent record types: https://www.cs.cornell.edu/people/kopylov/papers/dinter/dinter.pdf
@brad The DOT calculus also uses intersection for defining multifield classes - not sure what they use for the 'empty class' though.
@brendanzab yeah, I think it’s all a bit simpler the more I think about it. They’re really just sets with anonymous, extensible, records in them. I think. In the book they hand-wave the record stuff a bit tbh. The definition of joining says something like “just ‘set theory’ union the tuples”. But … the identity of a field (or component) of a tuple is a bit more complex than that suggests. I think.
Hmm, kind of suggests that it would be interesting to reframe it in terms of type theory to see what happens. I wonder if that has already been done before. 🤔