search

tomjaguarpaw / product-profunctors

Other
19 stars 14 forks source link

genericAdaptor does not infer #42

Open tomjaguarpaw opened 6 years ago

tomjaguarpaw commented 6 years ago

@hesselink I have hit a snag with genericAdaptor. It does not infer properly. For example, if I use p2 I get nice inference behaviour

> p2 (("hello " ++), reverse) ("world", [1..5])
("hello world",[5,4,3,2,1])

On the other hand, using genericAdaptor for the same purpose gives the error shown at the bottom of this comment. I managed to add a functional dependency which ends up giving us essentially a -> p. I think what we need is a -> p b c, p b c -> a. I can't see how to achieve this because Rep seems to get in the way.

Do you have any ideas how to address this? @Lysxia, you may also have some clever idea. about this.

Thanks!

genericAdaptor type error:

>  genericAdaptor (("hello " ++), reverse) ("world", [1..10])

<interactive>:11:2:
    Couldn't match expected type ‘GHC.Generics.M1
                                    GHC.Generics.D
                                    GHC.Generics.D1(,)
                                    (GHC.Generics.M1
                                       GHC.Generics.C
                                       GHC.Generics.C1_0(,)
                                       (GHC.Generics.M1
                                          GHC.Generics.S
                                          GHC.Generics.NoSelector
                                          (GHC.Generics.K1 GHC.Generics.R [Char])
                                        GHC.Generics.:*: GHC.Generics.M1
                                                           GHC.Generics.S
                                                           GHC.Generics.NoSelector
                                                           (GHC.Generics.K1 GHC.Generics.R [a1])))’
                with actual type ‘GHC.Generics.Rep a0’
    The type variables ‘a0’, ‘a1’ are ambiguous
    In the first argument of ‘print’, namely ‘it’
    In a stmt of an interactive GHCi command: print it
Lysxia commented 6 years ago

genericAdaptor here takes type genericAdaptor :: (String -> String, [Integer -> Integer]) -> (String, Integer) -> c, and the constraints deduce Rep c but that is not sufficient to deduce c itself since Rep is not an injective family.

It looks like instead of a -> p b c we should use Adaptor p a, which is less general but has better inference.

tomjaguarpaw commented 6 years ago

Great, thanks! I would indeed prefer this to be less general. I really want it to only work with types that look like Foo (p a b) (p a' b') -> p (Foo a b) (Foo a' b'). Your formulation via Adaptor p a has the properties that if we know a we know

Is there any hope of going the other way?

tomjaguarpaw commented 6 years ago

Oh, it doesn't seem to work, actually.

> genericAdaptor (("hello " ++), reverse) ("world", [1..5])

<interactive>:10:1:
    Could not deduce (Unzip 'Fst (,) ~ (,))
    from the context (Enum t,
                      Num t,
                      GHC.Generics.Generic (Unzip 'Fst (,) [Char] [t]),
                      GHC.Generics.Generic (Unzip 'Snd (,) [Char] [t]),
                      GHC.Generics.Rep (Unzip 'Fst (,) [Char] [t])
                      ~ GHC.Generics.M1
                          GHC.Generics.D
                          GHC.Generics.D1(,)
                          (GHC.Generics.M1
                             GHC.Generics.C
                             GHC.Generics.C1_0(,)
                             (GHC.Generics.M1
                                GHC.Generics.S
                                GHC.Generics.NoSelector
                                (GHC.Generics.K1 GHC.Generics.R [Char])
                              GHC.Generics.:*: GHC.Generics.M1
                                                 GHC.Generics.S
                                                 GHC.Generics.NoSelector
                                                 (GHC.Generics.K1 GHC.Generics.R [t]))),
                      GHC.Generics.Rep (Unzip 'Snd (,) [Char] [t])
                      ~ GHC.Generics.M1
                          GHC.Generics.D
                          GHC.Generics.D1(,)
                          (GHC.Generics.M1
                             GHC.Generics.C
                             GHC.Generics.C1_0(,)
                             (GHC.Generics.M1
                                GHC.Generics.S
                                GHC.Generics.NoSelector
                                (GHC.Generics.K1 GHC.Generics.R [Char])
                              GHC.Generics.:*: GHC.Generics.M1
                                                 GHC.Generics.S
                                                 GHC.Generics.NoSelector
                                                 (GHC.Generics.K1 GHC.Generics.R [t]))))
      bound by the inferred type of
               it :: (Enum t, Num t,
                      GHC.Generics.Generic (Unzip 'Fst (,) [Char] [t]),
                      GHC.Generics.Generic (Unzip 'Snd (,) [Char] [t]),
                      GHC.Generics.Rep (Unzip 'Fst (,) [Char] [t])
                      ~ GHC.Generics.M1
                          GHC.Generics.D
                          GHC.Generics.D1(,)
                          (GHC.Generics.M1
                             GHC.Generics.C
                             GHC.Generics.C1_0(,)
                             (GHC.Generics.M1
                                GHC.Generics.S
                                GHC.Generics.NoSelector
                                (GHC.Generics.K1 GHC.Generics.R [Char])
                              GHC.Generics.:*: GHC.Generics.M1
                                                 GHC.Generics.S
                                                 GHC.Generics.NoSelector
                                                 (GHC.Generics.K1 GHC.Generics.R [t]))),
                      GHC.Generics.Rep (Unzip 'Snd (,) [Char] [t])
                      ~ GHC.Generics.M1
                          GHC.Generics.D
                          GHC.Generics.D1(,)
                          (GHC.Generics.M1
                             GHC.Generics.C
                             GHC.Generics.C1_0(,)
                             (GHC.Generics.M1
                                GHC.Generics.S
                                GHC.Generics.NoSelector
                                (GHC.Generics.K1 GHC.Generics.R [Char])
                              GHC.Generics.:*: GHC.Generics.M1
                                                 GHC.Generics.S
                                                 GHC.Generics.NoSelector
                                                 (GHC.Generics.K1 GHC.Generics.R [t])))) =>
                     Unzip 'Snd (,) [Char] [t]
      at <interactive>:10:1-57
    Expected type: ([Char], [t]) -> Unzip 'Snd (,) [Char] [t]
      Actual type: Unzip 'Fst ([Char] -> [Char], [t] -> [t])
                   -> Unzip 'Snd ([Char] -> [Char], [t] -> [t])
    The function ‘genericAdaptor’ is applied to two arguments,
    its type is ‘Adaptor p0 a0’,
    it is specialized to ‘Adaptor (->) ([Char] -> [Char], [t] -> [t])’
    In the expression:
      genericAdaptor (("hello " ++), reverse) ("world", [1 .. 5])
    In an equation for ‘it’:
        it = genericAdaptor (("hello " ++), reverse) ("world", [1 .. 5])
Lysxia commented 6 years ago

It seems instances of Unzippable (which defines Unzip) are missing for the standard types, which would cause that error for GHC < 8.

instance Unzippable (,)