Feature request: named function's arguments

[Pitometsu]

With row-types it's possible to pass some named parameters to function. But what about partial application? Would it make sense to implement .-> type indexed by parameter name? "Int .-> "x" Float .-> "y" () (Or? ("x", Int) .-> ("y", Float) .-> ())

Additional feature: optional parameters. E.g. via some typeclass mark some field as optional, wrap them to Maybe if missed. Optional '["x"] => Rec ("x" .== Int .+ "y" .== Float) -> (). Though not sure here. It must behave like Rec ("y" .== Float) -> () for caller, and Rec ("x" .== Maybe Int .+ "y" .== Float) -> () for function implementation body. "Int .?> "x" Float .-> "y" () (Or? ("x", Int) .?> ("y", Float) .-> ())

[Pitometsu]

Something like

type family (.->) :: (Symbol, Type) -> Type -> Type where
  (label, a) .-> b = Rec (label .== a) -> b

[dwincort]

I'm not exactly sure how partial application would work. Is this just a short-hand for writing the type signature? Like, are you imagining a type family that you write like ("x", Int) .-> ("y", Float) .-> Bool but that desugars to Rec ("x" .== Int .+ "y" .== Float) -> Bool? That might be possible, but I'm not exactly sure what it brings to the table.

Speaking of partial application, maybe you're thinking more along the lines of a curry function? Something like:

curryRec :: forall l t r x. KnownSymbol l => (Rec (l .== t .+ r) -> x) -> t -> Rec r -> x
curryRec f t r = f $ (Label @l .== t) .+ r

That's a pretty straightforward function, but maybe it's worth adding.

---

Optional parameters are an interesting idea, but I can't seem to figure them out with some really ugly overlapping instances. My current work in progress looks like:

class Optional (l :: Symbol) (a :: k) (r :: Row k) where
  optional :: Maybe (Dict (r .! l ≈ a))

instance Optional l a Empty where
  optional = Nothing

instance {-# OVERLAPPING  #-} Optional l a ('R (l :-> a ': r)) where
  optional = Just Dict

instance {-# OVERLAPPABLE  #-} Optional l a ('R (l :-> b ': r)) where
  optional = Nothing

instance {-# OVERLAPPABLE #-} (Optional l a ('R r), Get l ((l' :-> b) : r) ~ Get l r) => Optional l a ('R (l' :-> b ': r)) where
  optional = case optional @_ @l @a @('R r) of
    Nothing -> Nothing
    Just Dict -> Just Dict

As an example of using it, you could imagine a function like:

foo :: forall r. (Optional "x" Int r, HasType "y" Int r) => Rec r -> Int
foo r = case optional @_ @"x" @Int @r of
  Nothing -> r .! (Label @"y")
  Just Dict -> (r .! (Label @"y")) + (r .! (Label @"x"))

With my brief testing, this works, but the error messages can get really terrible. One of the nice things about the row-types library right now is that it doesn't use any overlapping instances (which makes the error messages better). I like this idea though, so I'll mull it over and see if I can figure out a way to make it work a little more elegantly.

[Pitometsu]

Speaking of partial application, maybe you're thinking more along the lines of a curry function? Something like: ...

Yes, exactly. Actually I thinking of analogous to Caml's named arguments.

[dwincort]

Yeah, ok, we can do something like Caml's named arguments. Consider this function:

infixl 3 .$
(.$) :: forall l t r r' x. (KnownSymbol l, r' .! l ≈ t) => (Rec (l .== t .+ r) -> x) -> (Label l, Rec r') -> Rec r -> x
(.$) f (l, r') r = f $ (l .== (r' .! l)) .+ r

Now, we can construct a simple example:

xtheny :: Rec ("x" .== String .+ "y" .== String) -> String
xtheny r = (r .! #x) ++ (r .! #y)

greeting = #x .== "hello " .+ #y .== "world!"

And if we play around with this, we can do:

> xtheny greeting
"hello world!"
> xtheny .$ (#x, greeting) .$ (#y, greeting) $ empty
"hello world!"
> xtheny .$ (#y, greeting) .$ (#x, greeting) $ empty
"hello world!"
> xtheny .$ (#y, greeting) .$ (#x, #x .== "Goodbye ") $ empty
"Goodbye world!"

(Also, for the record, you don't need the type signature on xtheny. Even the inferred type of xtheny :: ((r .! "x") ~ [a], (r .! "y") ~ [a]) => Rec r -> [a] works just fine.)

[dwincort]

I thought about Optional a little more, and the fundamental issue is that there's no easy way to do type equality at the value level without a Typeable constraint, which I don't really want to add. One way is with overlapping instances, which I showed above. I came up with another that uses type families and symbols, but it's also a little ugly:

type family TypeEq (a :: k) (b :: k) :: Symbol where
  TypeEq a a = "True"
  TypeEq a b = "False"

-- | This is a hack to get type equality without using 'Typeable'.  It relies on
-- the fact that the type family 'TypeEq' is closed, but it still may fail when
-- 'TypeEq' can't properly reduce (for instance, in the presence of some polymorphism).
typeEq :: forall a b. KnownSymbol (TypeEq a b) => Maybe (a :~: b)
typeEq = case sameSymbol (Proxy @(TypeEq a b)) (Proxy @"True") of
  Just Refl -> Just $ UNSAFE.unsafeCoerce Refl
  Nothing -> Nothing

Since the type family is closed, the unsafeCoerce should be fine, but as I wrote in the comment, this can still fail during type checking due to polymorphism just as the overlapping instances version does. However, the error is maybe nicer? Instead of complaining about overlapping instances, it says:

error:
    * No instance for (KnownSymbol (Data.Row.Internal.TypeEq t1 t2))
        arising from a use of ...

It would be really cool if I could use custom type errors to make this error print out something specific about Optional failing when type polymorphism prevents type equality checking, but that doesn't seem possible (both because KnownSymbol is a special class and because I would be trying to make an instance where the head was a type family).

Of course, that's not all I needed to make Optional free of overlapping instances. I also had to do some more safe unsafeCoerces:

-- | Like 'sameSymbol', but if the symbols aren't equal, this additionally provides
-- proof of LT or GT.
cmpSymbol :: (KnownSymbol a, KnownSymbol b)
          => Proxy a -> Proxy b -> Either (a :~: b) (Either (Dict (CmpSymbol a b ~ 'LT)) (Dict (CmpSymbol a b ~ 'GT)))
cmpSymbol x y = case compare (symbolVal x) (symbolVal y) of
  EQ -> Left (UNSAFE.unsafeCoerce Refl)
  LT -> Right (Left  (UNSAFE.unsafeCoerce $ Dict @Unconstrained))
  GT -> Right (Right (UNSAFE.unsafeCoerce $ Dict @Unconstrained))

-- | 'Get' is preserved through a row-type so long as the label isn't yet found.
preserveGet :: forall l l' a r. ((l' <=.? l) ~ True) :- (Get l (l' :-> a ': r) ~ Get l r)
preserveGet = Sub $ UNSAFE.unsafeCoerce $ Dict @((l' <=.? l) ~ True)

Honestly, cmpSymbol seems like something that could be upstreamed. With all of this machinery in place, I can define:

class Optional (l :: Symbol) (a :: k) (r :: Row k) where
  optional :: Maybe (Dict (r .! l ≈ a))

instance Optional l a Empty where
  optional = Nothing

instance (KnownSymbol l, KnownSymbol l', Optional l a ('R r), KnownSymbol (TypeEq a b)) => Optional l a ('R (l' :-> b ': r)) where
  optional = case (cmpSymbol (Proxy @l') (Proxy @l), typeEq @a @b, optional @_ @l @a @('R r)) of
    -- The labels are equal and the types at those labels are equal.
    (Left Refl, Just Refl, _) -> Just Dict
    -- The label we're looking for is deeper in the row
    (Right (Left Dict), _, Just Dict) -> Just Dict \\ preserveGet @l @l' @b @r
    _ -> Nothing

---

Long story short, I'm still not sure about this one. Despite the complexity, I think this newer version is a definite improvement given that it doesn't need overlapping instances. That said, the fact that it simply doesn't work in the face of polymorphism is pretty bad. I could fix this by adding Forall Typeable r to the instance constraint, but that adds a considerable burden to anyone who wants to use Optional.

[dwincort]

The main reason I've been struggling with Optional is the scenario where you have a record like:

rec :: Rec ("x" .== Integer .+ "y" .== String)
rec = (#x .== 4 .+ #y .== "string")

and a function of type:

foo :: (HasType "x" Integer r, Optional "y" Integer r) => Rec r -> Integer

Should rec be a valid argument to foo? My initial assumption was yes — foo demands that the field at label "x" be an Integer, but since the field at label y is optional, it shouldn't matter that rec has a field at label "y" of type String. But, to achieve this, I need type equality, and without using Typeable (and it would be required for all fields in r), the best I can do is have it work when types are concrete. So, foo rec would work, but foo rec' wouldn't:

rec' :: Num n => Rec ("x" .== Integer .+ "y" .== n)
rec' = (#x .== 4 .+ #y .== 3)

But another option is to try to design it so that rec' works but rec doesn't. I could add a constraint to Optional which enforces that if the input row-type has the label "y" at all, then it must have type Integer. Then, foo rec would not type check because String /= Integer, but foo rec' would work, because the type checker would deduce that n must be Integer.

That leaves me with three potential versions.

1. Polymorphism doesn't work (foo rec works but foo rec' doesn't).
2. Optional restricts the record type at the optional label (foo rec' works but foo rec doesn't).
3. Optional enforces Typeable on every field in the record (both foo rec and foo rec' work, assuming rec' additionally has a Typeable n constraint).

@Pitometsu, since you're the one who suggested this idea, I'm curious if you have a preference.

[Pitometsu]

Thank you for asking. Case 2 make sense to me, because library already have assumption that records must have no several rows with same label, which mach nicely to design. Case 3 could co-exist, maybe, but not sure when it could be useful. As for me it's ok for user to explicitly upcast the record in case of label naming conflict, because function's result type might contain the function's expected row of it's expected type, not the record's one in case of conflict (and can't both, obviously).

foo' ::
  ( HasType "x" Integer r, Optional "y" Integer r
  , HasType "x" Integer r', HasType "y" (Maybe Integer) r' ) => Rec r -> Rec r'

*However in exposed example there's no row-polymorphism. Not sure how to describe it with Optional. Maybe:

foo' :: (HasType "x" Integer r, Optional "y" Integer r)
  => Rec r -> Rec (Modify r "y" (Maybe Integer))

[dwincort]

Now that I went to code it up, I totally agree that option 2 makes the most sense:

class Optional (l :: Symbol) (a :: k) (r :: Row k) where
  optional :: Maybe (Dict (r .! l ≈ a))

instance Optional l a Empty where
  optional = Nothing

instance ( KnownSymbol l, KnownSymbol l', Optional l a ('R r)
         , Ifte (CmpSymbol l l' == 'EQ) (a ~ b) Unconstrained
         , Ifte (l' <=.? l) (Get l r ~ Get l (l' :-> b ': r)) Unconstrained
  ) => Optional l a ('R (l' :-> b ': r)) where
  optional = case (cmpSymbol (Proxy @l') (Proxy @l), optional @_ @l @a @('R r)) of
    -- The labels are equal and the types at those labels are equal.
    (Left Refl, _) -> Just Dict
    -- The label we're looking for is deeper in the row
    (Right (Left Refl), Just Dict) -> Just Dict
    _ -> Nothing

Aside from some weird constraints in the instance context (which don't seem to have any effect on using Optional), it's surprisingly clean — it uses the cmpSymbol function (which I'm also trying to upstream), but there's no other need for unsafeCoerce.

Also, I was able to write your upcastOptional function :).

upcastOptional :: forall l a r. (Optional l a r, KnownSymbol l) => Rec r -> Rec ((l .== Maybe a) .// r)
upcastOptional r = case optional @_ @l @a @r of
  Nothing -> (l .== Nothing @a) .// r
  Just Dict -> (l .== Just (r .! l)) .// r
  where l = Label @l

with pretty nice behavior:

> testrec :: Num n => Rec ("x" .== n .+ "z" .== String)
> let testrec = (#x .== 4 .+ #z .== "foo")
> upcastOptional @"y" testrec
#x .== 4 .+ #y .== Nothing .+ #z .== "foo"
> upcastOptional @"a" testrec
#a .== Nothing .+ #x .== 4 .+ #z .== "foo"
> upcastOptional @"z" testrec
#x .== 4 .+ #z .== Just "foo"

[Pitometsu]

Amazing results, and the great work, thank you! Though upcastOptional looks handy, I, probably, should clarify a little what I mean is: by upcast it meant just casting by hand in each specific case from e.g. Rec $ "x" .== Integer .+ "y" .== String to Rec $ "x" .== Integer in case of passing it to function with Optional "y" Integer r. So I see there's no way to have a function that automate it, I guess. On other hand it probably possible to make a type family to create a result row like ((l .== Maybe a) .// r (return rows type with optionalized row would, probable, an often case). Something like:

type family UpcastOptional (l :: Symbol) (r :: Row k):: Row k where
  (Optional l a r, a ≈ r .! l) => (l .== Maybe a) .// r

BTW, what do you think, would be Optional and UpcastOptional versions for several optional rows be handy as well (like Subset for HasType)?

[dwincort]

Ahh, I think I see what you're saying: your idea for an automated upcast is about removing a field from a record if and only if the type at that record doesn't match the Optional? I'm pretty sure this once again comes down to the issue of type equality, so yeah, I don't think I can automate it in the general case.

I'm not sure I understand this UpcastOptional type family you're proposing. First off, that's not valid type family syntax. Are you trying to make a type synonym for (l .== Maybe a) .// r, or is it something more complicated? If it's more complicated, please try to explain what else UpcastOptional should be doing. If it's basically just a type synonym, then why not just use (l .== Maybe a) .// r?

[Pitometsu]

I thought about the way to automate result type (which contains Maybe rows) receiving, because we already know the type of record and type class of optionals (there's would be a lot of .== Maybe in case of several optional fields). E.g. we can use something like

:: ( os ~ "x" .== Int .+ "y" .== Float .+ "z" .== Bool
   , Optionals os r ) => Rec r -> UpcastOptionals os r

[Pitometsu]

Oh, I see a package with named arguments http://hackage.haskell.org/package/named

row-types could have an integration for curried ones.