Chart path to row types

nfrisby commented 5 years ago

What will it take to associate a type with each frag element?

This is already possible to a limited degree, right now. If the label alone determines the type and you know them all, then you can use a data/type family as/within the functor argument to Prod and Sum. But that's a disappointing limitation -- we want extensibility and anonymity here too.

I'm hoping the answer isn't just "duplicate all the frag machinery but on type-level pairs and unify the second part whenever the first part matches". Even in that case, does the SetFrag constraint prevent any ambiguity regarding interleavings of insertions/deletions, or will that require additional care?

Two ideas:

Require the codomain of a row type to be an abelian group? E.G. type-level integer. E.G. notably a frag. Abelian is weird requirement for row type codomains, though.

Another special data kind. This one is not a group. It would require #5: frags in kinds.

data Row (ks :: Frag (dom :: kdom)) (cod :: kcod)
type family Ext (p :: Row (ks :: Frag dom) cod) (k :: dom) (v :: cod) :: Row (ks :+ k) cod
type family Get (k :: dom) (p :: Row (ks :: Frag dom) cod) :: cod

Get k (Ext p k v) ~ v
Get k (Ext p j v) ~ Get k p   if Apart k j

emp :: Record (p :: Row 'Nil cod) f
ext :: (SetFrag ks,FragEQ k ks ~ 'Nil,KnownFragCard (FragLT k ks))
    => Record (p :: Row ks cod) f -> f k v -> Record (Ext p k v) f
rem :: (SetFrag ks,FragEQ k ks ~ 'Nil,KnownFragCard (FragLT k ks)))
    => proxy k -> Record (Ext p k v) f -> Record (p :: Row ks cod) f
p ~ q :: Row ks cod   iff   (SetFrag ks,forall k in ks. Get k p ~ Get k q)

data Record :: Row (ks :: Frag dom) cod -> (dom -> cod -> Type) -> Type where
    MkNil :: Record (p :: Row 'Nil cod) f
    MkCons ::
      (FragEQ k ks ~ 'Nil,FragLT k ks ~ 'Nil)
      => Record (p :: Row ks cod) -> f k v -> Record (Ext p k v)   -- TODO need kind-driven eta-expansion

Note that we don't even need 'Emp :: Row 'Nil cod, let alone Rem k p. But it might be nicer to have them anyway. The basic idea is to let Frag handle all the interesting constraints, so that the frag-index on Row drives its shape via eta-reduction.

nfrisby commented 5 years ago

I came up with a simpler idea on pen and paper. Just use the function's graph as a frag.

infix 7 :=
data Mapping dom cod = To dom cod
type (:=) = To

type family DomFrag (fr :: Frag (Mapping dom cod)) :: Frag dom where {}

The key ingredient is a special rule in envMultiplicity: if all multiplicities in p are non-negative, then the multiplicity of k := v in p is at most the multiplicity of k in DomFrag p.

I'm trying this now.

nfrisby commented 5 years ago

I pushed branch issue/19-domfrag. It has a first attempt at Record, using DomFrag.

It went according to the pen and paper plan, except for the type of Data.Motley.Row.ret (and thereby prj and rmv).

Without FragEQ (lbl := a) p ~ 'Nil, we are attempting the following.

have:
      FragEQ lbl (DomFrag p) ~ 'Nil
      SetFrag (DomFrag (p :+ lbl := a)) ~ '()
      SetFrag (p :+ lbl := a) ~ '()

want:
      FragEQ (lbl := a) p ~ 'Nil

which simplifies to

have:
      FragEQ lbl (DomFrag p) ~ 'Nil
      SetFrag (DomFrag p)

      SetFrag (FragNE (lbl := a) p)
      SetFrag (FragEQ (lbl := a) p :+ '())   -1 <= p(lbl := a) <= 0

want:
      FragEQ (lbl := a) p ~ 'Nil

That doesn't currently work. I think it's because the current implementation is conservative because p could for example be

  'Nil :+ lbl := b :- lbl := a

for some b /~ a.

I need to go back to pen and paper to determine if that is overly conservative, and how to update the constraint simplifier to be less conservative. If it's not overly conservative, then maybe DomFrag is the wrong approach. Perhaps a FragNEArg lbl p ~ p instead... seems heavier though.

Edit: I'm now thinking FragEQ (k := v) p ~ 'Nil might actually be the correct constraint for functions that remove a field from a row. Note that ext uses FragEQ k (DomFrag p) ~ 'Nil. I wasn't expecting an asymmetry, but maybe it's just unexpected, not wrong. I think I need to try using the interface for some actual work before I'll be able to tell.

Edit 2: I think DomFrag suffices for a quite a bit, but it is ultimately incomplete compared to FragEQArg, FragNEArg :: dom -> Frag (Mapping dom cod) -> Frag (Mapping dom cod): counting doesn't cut it. Then FunFrag (p :+ k := a) = (FunFrag (FragNEArg k p),FragEQArg k p ~ 'Nil). I need to come up with example programs.

nfrisby commented 5 years ago

I merged the function graph approach using only Frag constraints plus DomFrag into develop at commit 94dd754. Closing.

nfrisby / frags

Chart path to row types #19