да, но у меня ещё 0.12

мм, а чем мой пример с Exists не подошёл? тем, что нужно иметь некое общее "представление"?

потерял связь со своим примером, разбираюсь и с этим тоже. потому что абстрагировал свой из реальной задачи, теперь собираю обратно картину)

Он — компилится

ну там тоже мапа, в неё можно класть разные штуки :)

твой пример с exists требует дополнительный ADT

можно использовать любой существующий тип вместо него
ну да, вообще да, требует

ну и дополнительный тайпкласс

data Rep = RepI Int | RepS String

class HasRep a where rep ∷ a → Rep

data Foo a = Foo a (a → Rep)
type FooE = Exists Foo

mkFooE :: forall a. (HasRep a) => a -> FooE
mkFooE a = mkExists (Foo a rep)

newtype FooMap k = FooMap (Map k FooE)

newtype X = X Int
newtype Y = Y String

instance hasRepX ∷ HasRep X where rep (X n) = RepI n
instance hasRepY ∷ HasRep Y where rep (Y s) = RepS s

foos' ∷ FooMap String
foos' = FooMap
  $ Map.insert "y" (mkFooE $ Y "y")
  $ Map.singleton "x" (mkFooE $ X 1)

Удалось переработать под мою задачу, спасибо!

Примерно так вышло:

class MyClass c d where rep ∷ c → d

data Foo d c = Foo c (c -> d)
type FooE d = Exists (Foo d)

mkFooE :: forall c d. (MyClass c d) => c -> FooE d
mkFooE a = mkExists (Foo a rep)

newtype DifferentFoos d = DifferentFoos (Map String (FooE d))

newtype X = X Int
newtype Y = Y String

data F = G | H

instance myClassXF ∷ MyClass X F where rep (X n) = G
instance myClassYF ∷ MyClass Y F where rep (Y s) = H

foos' ∷ DifferentFoos F
foos' = DifferentFoos
  $ Map.insert "y" (mkFooE $ Y "y")
  $ Map.singleton "x" (mkFooE $ X 1)

^ исправил на DifferentFoos F, так будет работать

зачем это? data F = G | H?
тогда вообще можно просто data XY = X Int | Y String
и в мапу все будет ложиться

мне важно, чтобы F (d) был общим для всех значений, а вариативность нужна по X и Y (c), важно чтобы их можно было создать динамически и засунуть в Map

это не универсально, будет 3 конструктора и надо будет твой F расширять

https://www.youtube.com/playlist?list=PLO46zvIozaIpZBhU85uvJXPg0PMmU-2ZY
(эх, у первого доклада тёмные слайды и почти во всех плохой звук)

class MyClass c d where rep ∷ c → d

data Foo d c = Foo c (c -> d)
type FooE d = Exists (Foo d)

mkFooE :: forall c d. (MyClass c d) => c -> FooE d
mkFooE a = mkExists (Foo a rep)

newtype DifferentFoos d = DifferentFoos (Map String (FooE d))

newtype X = X Int
newtype Y = Y String

data F = G | H

instance myClassXF ∷ MyClass X F where rep (X n) = G
instance myClassYF ∷ MyClass Y F where rep (Y s) = H

foos' ∷ DifferentFoos F
foos' = DifferentFoos
  $ Map.insert "y" (mkFooE $ Y "y")
  $ Map.singleton "x" (mkFooE $ X 1)

Немного другой вариант, попроще, просто для истории, необходимо было, чтобы X и Y тоже могли быть data, не только newtype

class MyClass d c where fn ∷ c → d

data Foo d c = Foo { f1 :: c, f2:: d }
type FooE d = Exists (Foo d)

mkFooE :: forall d c. (MyClass d c) => Foo d c -> FooE d
mkFooE = mkExists

newtype DifferentFoos d = DifferentFoos (Map.Map String (FooE d))

data X = XZ | XW
data Y = YQ | YU

data F = FG | FH

instance myClassXF ∷ MyClass F X where fn _ = FG
instance myClassYF ∷ MyClass F Y where fn _ = FH

foos' ∷ DifferentFoos F
foos' =
    let
        fooA :: Foo F X
        fooA = Foo { f1 : XZ, f2 : FG }
        fooB :: Foo F Y
        fooB = Foo { f1 : YQ, f2 : FH }
    in
        DifferentFoos
            $ Map.insert "y" (mkFooE fooA)
            $ Map.singleton "x" (mkFooE fooB)

вопросик

какая форма койонеды будет через двойной ранг forall?

надо проверить на то, что это справедливо

только сегодня понял смысл леммы Йонеды, так что я точно не смогу это проверить, но я теперь хоть могу интерпретировать как-то эти буковки частично
во всяком случае теперь (b -> a) (f b) мне понятно

ну лемма Йонеды, теорема Кели это все про одно и тоже