Update functional dependencies so multiple operations can be supported on the same underlying record

[thomashoneyman]

Currently, purescript-heterogeneous allows you to create functions like these:

-- Count the number of `Either` values in a record that are `Left`
data CountLeft = CountLeft

instance countLeft :: Folding CountLeft Int (Either a b) Int where
  folding CountLeft acc (Left _) = acc + 1
  folding CountLeft acc _ = acc

countLefts :: forall r. HFoldl CountLeft Int { | r } Int => { | r } -> Int
countLefts = hfoldl CountLeft 0

-- Count the number of `Either` values in a record that are `Right`
data CountRight = CountRight

instance countRight :: Folding CountRight Int (Either a b) Int where
  folding CountRight acc (Right _) = acc + 1
  folding CountRight acc _ = acc

countRights :: forall r. HFoldl CountRight Int { | r } Int => { | r } -> Int
countRights = hfoldl CountRight 0

But what if you want a function that uses multiple operations?

countBoth :: forall r.
  HFoldl CountLeft Int { | r } Int =>
  HFoldl CountRight Int { | r } Int =>
  { | r } ->
  Int
countBoth r = countRights r + countLefts r

This ought to be valid, but instead causes a compiler error. A record can only match one instance!

Solution

This PR updates the functional dependencies for the HFoldl and HMap classes (with help from @MonoidMusician) and provides test cases proving that the new functional dependencies support this use case.

[thomashoneyman]

Curiously -- though I'm not sure exactly why -- this does not work:

class HFoldlWithIndex f x a b | f x a -> b where

[thomashoneyman]

@MonoidMusician noticed that, after updating the functional dependencies, it's also necessary to annotate this now. This makes the library a little less user-friendly in that inference will nicely cover less cases.

[thomashoneyman]

I haven't been able to figure out why the RowToList and MapRecordWithIndex constraints are necessary. In addition, it's extremely brittle: MapRecordWithIndex rs (ReplaceLeft rvals) rout rout does not work, for example.

[thomashoneyman]

Unfortunately, putting these as multiple constraints on a large function (as in thomashoneyman/purescript-halogen-formless@0811a64) completely messes up type checking when that function is used.

Clearly my solution as provided here is not actually solving the problem, though it appears to on the tests that I've added in this module.

Context

I’m mounting a component:

Halogen.HTML.slot unit Formless.component ?abc (const Nothing)

Now, I’m supposed to provide an argument where I’ve placed ?abc of this type:

type Input f = { initialInputs :: f Record InputField, ... }

I’ve gone ahead and made one using the explicit / verbose format:

initialInputs :: ContactForm Record InputField
initialInputs = ContactForm { name: InputField "", text: InputField "" }

the component has explicitly been told that f is ContactForm, so there’s no trouble there. The input has the right type. However, if I try to use it…

Halogen.HTML.slot unit Formless.component { initialInputs, ... } (const Nothing)

…I get an error:

Error 1 of 3:

  in module Example.Basic.Component
  at example/basic/Component.purs line 43, column 20 - line 43, column 31

    Could not match type

      String

    with type

      InputField FieldError String String


  while trying to match type 
      ( name :: String
      , text :: String
      )
    with type 
      ( name :: InputField FieldError String String
      , text :: InputField Void String String
      )
  while solving type class constraint

    Prim.Row.Cons "name"
                  t4
                  t5
                  ( name :: InputField FieldError String String
                  , text :: InputField Void String String
                  )

  while checking that expression component
    has type Component HTML t0 t1 t2 t3

Strangely, the compiler appears to believe I’ve provided something of type { name :: String, text :: String }. But I have clearly provided the type that it wants — { name :: InputField FieldError String String, text :: InputField Void String String }. If I explicitly provide something wrong — like a halfway-correct { name :: String, text :: InputField Void String String }, the compiler picks up that this is wrong and correctly notes the types.

This happens even if I just put ?abc and don’t even bother attempting to provide something of the right type. It appears that no matter what I provide, the compiler will believe it is not acceptable. So that leads me to believe there’s something up with one of my constraints on the component.

---

For context, here's the component, though it's a gnarly type signature:

component
  :: ∀ form is fs fxs
   . Monad m
  => RL.RowToList fs fxs
  => HMap GetInputField { | fs } { | is }
  => HMap SetFormFieldTouched { | fs } { | fs }
  => MapRecordWithIndex fxs (ReplaceInput is) fs fs
  => HFoldl CountError Int { | fs } Int
  => HFoldl Touched Boolean { | fs } Boolean
  => Newtype (form Record InputField) { | is }
  => Newtype (form Record FormField) { | fs }
  => Component ParentQuery ChildQuery ChildSlot form m

---

In the end, I reverted the changes and went back to a more primitive RowToList approach. I'm not sure exactly what the source of this issue is.

[natefaubion]

Thank you for looking into this. I've made a followup commit which will clean things up a little bit. 0ba771a

To go into more detail. The crux of the issue is that with the old functional dependencies a -> f x b, only one combination of folding function and initial accumulator can be used for a given input in a given context. This appears to infer well because all you need is the input type (which is almost always known) to dispatch, with a glaring downside.

I actually think one way around it would be to use a fresh type variable for the input type, with TypeEquals coercions. I think this would still let us determine everything by a single input, and you only have to annotate which type variable it maps to. I might explore this some, because if you can even just annotate your folding/mapping type with the carrier type, you can avoid some of the confusion around what else to annotate.

In that commit, I've just fixed everything to the more general dependencies of f x a -> b, which means we determine the output from any combination of folding function, accumulator, and input. This is what we expect at the value level for something like foldr, so it makes sense. However that means that the compiler absolutely will not infer any of these types, so you have to annotate exactly all these arguments in some way. This clears up a lot of the confusion about the behavior and why some things work and some things don't.

In your replaceLeft/replaceRight combo, the reason you are having trouble is because, while you know that the output of both functions is { | rout }, the compiler does not. To the compiler, the outputs of each function are actually { | rout1 } and { | rout2 }. So while you know they should map to the same thing, to the compiler they are unique outputs (fresh type variables), and your other constraints are just a roundabout way of asserting that equality. If you embrace the fact that they are technically independent variables, the type signature and annotations are what you'd expect.

[thomashoneyman]

In your replaceLeft/replaceRight combo, the reason you are having trouble is because, while you know that the output of both functions is { | rout }, the compiler does not. To the compiler, the outputs of each function are actually { | rout1 } and { | rout2 }.

I find that surprising -- wouldn't the type signature below assert to the compiler that the output row of both constraints is in fact the same row? Why would the compiler consider them to be actually { | rout1 } and { | rout2 }?

If the compiler considers them to be { | rout1 } and { | rout2 } then perhaps I am misunderstanding what exactly this is asserting.

  HMapWithIndex (ReplaceLeft rvals) { | rin } { | rout } =>
  HMapWithIndex (ReplaceRight rvals) { | rin } { | rout } =>

---

Aside from my questions, is there anything else that ought to happen in order to merge this? It seems that at least a README update could be included to note the new need to annotate some types.

[natefaubion]

The issue is that you are feeding the result of one into the next. Your constraints say it goes from rin to rout, but then you feed rout into the next one, yet you've labelled it as taking rin. Therefore you'd need evidence that rin ~ rout which doesn't exist with these constraints alone. Your other constraints basically derive rin ~ rout.

[natefaubion]

If you want to merge my branch into yours, and update the README, I'll merge it.

[thomashoneyman]

Ah! That does make sense, in retrospect, especially looking at your adjustment in 0ba771a.

My understanding of what these type variables mean is indistinct; I usually consider rin to be the same as rout if the labels and types associated with them are identical. I would expect that in the replaceLeft / replaceRight example that all of them could just be the same type variable. Clearly that's not correct.

Do you have a better intuition for what makes rin / rmid / rout distinct from one another? Is there a particular reason why I can't assert that all three are the same by using the same variable throughout?

[natefaubion]

You can use the same variable. This type checks.

testReplaceBoth :: forall rvals r.
  HMapWithIndex (ReplaceLeft rvals) { | r } { | r } =>
  HMapWithIndex (ReplaceRight rvals) { | r } { | r } =>
  { | rvals } ->
  { | r  } ->
  { | r }
testReplaceBoth vals =
  replaceLeft vals >>> replaceRight vals

But you didn't do that 😄, if you use distinct type variables, then they are distinct to the compiler. The only way to have them unify again is through some sort of equality.

[thomashoneyman]

I'll update the readme.

[thomashoneyman]

@natefaubion Updated!

[natefaubion]

Thanks!