I think that embedding one row in another can be done right now with type classes with the current basic interface, but I suspect that an Includes relation would be better behaved, especially alongside row polymorphism.
Includes p q would mean that p has every column that q has, enabling primitives like rupcast :: R f p -> R f q and vupcast :: V f q -> V f p. I anticipate that the necessary evidence would be a bitvector with as many bits as columns in p, each set if that field is in q.
Some non-trivial examples that I anticipate the plugin being able to decide:
Includes (p .& l .= t) p.Includes (p .& l .= t1) (q .& l .= t2) implies t1 ~ t2.- Not
Includes p (q .& l .= t) if Lacks p l.
Includes p q and Includes q r implies Includes p r.
(Is there a "closure" of this where a column in q can be present with a different type in p if it is a Row type and the column type in p Includes the column type in q?)
I think that embedding one row in another can be done right now with type classes with the current basic interface, but I suspect that an
Includesrelation would be better behaved, especially alongside row polymorphism.Includes p qwould mean thatphas every column thatqhas, enabling primitives likerupcast :: R f p -> R f qandvupcast :: V f q -> V f p. I anticipate that the necessary evidence would be a bitvector with as many bits as columns inp, each set if that field is inq.Some non-trivial examples that I anticipate the plugin being able to decide:
Includes (p .& l .= t) p.Includes (p .& l .= t1) (q .& l .= t2)impliest1 ~ t2.Includes p (q .& l .= t)ifLacks p l.Includes p qandIncludes q rimpliesIncludes p r.(Is there a "closure" of this where a column in
qcan be present with a different type inpif it is aRowtype and the column type inpIncludesthe column type inq?)