Как дать GHC подсказку для построения QuantifiedConstraints? - PullRequest
Новая
       19

Как дать GHC подсказку для построения QuantifiedConstraints?

0 голосов
/ 27 декабря 2018

Если у меня есть метод: 

proveBar :: forall x . SingI x => Dict (Barable (Foo x))
proveBar = ...

Тогда как передать это как контекст: 

useBar :: forall foo . (forall x. SingI x => Barable (foo x)) => ...
useBar = ...

привязка foo к Foo?

Dict определено здесь https://hackage.haskell.org/package/constraints-0.10.1/docs/Data-Constraint.html#g:2

1 Ответ

0 голосов
/ 28 декабря 2018

Вы не можете с тем, что у вас есть.

Для того, чтобы использовать useBar с foo ~ Foo, вам нужны доказательства того, что (forall x. SingI x => Barable (Foo x)).

Сопоставление с образцом на proveBar не будет работать, потому что к тому времени, когда вы совпадете с Dict, x больше не будет универсально квалифицированным;вы ограничили x определенным (неуказанным) типом.

Что вам действительно нужно, так это соответствие шаблону типа Dict (forall x. SingI x => Barable (Foo x)), но этот тип в настоящее время не поддерживается GHC: 

• Illegal polymorphic type: forall x. SingI x => Barable (Foo x)
  GHC doesn't yet support impredicative polymorphism
• In the type signature: proveBar' :: Dict (forall x. SingI x => Barable (Foo x))

Если бы вместо этого у вас было свидетельство формы 

proveBar :: SingIBarable Foo

data SingIBarable foo where
  SingIBarable :: (forall x. SingI x => Barable (foo x)) -> SingIBarable foo

Тогда вы сможете использовать useBar при сопоставлении с шаблоном proveBar.

...