Можно ли «разогнать» полный квантор?

Предположим, что у нас есть конструктор типа f, который принимает два типа с помощью пары, созданной DataKinds.Можно ли «разогнать» полный квантор?

forall (f :: (ka, kb) -> *)

Затем я могу реализовать функцию forward, которая подобна curry для forall квантификатора:

forward :: forall (f :: (ka, kb) -> *). 
      (forall (ab :: (ka, kb)).  f ab) -> 
      (forall (a :: ka) (b :: kb). f '(a, b)) 
forward x = x

Однако обратная функция является проблематичным:

backward :: forall (f :: (*, *) -> *). 
      (forall (a :: *) (b :: *). f '(a, b)) -> 
      (forall (ab :: (*, *)). f ab) 
backward x = x

GHC 8.0.1 выдает сообщение об ошибке:

 
    • Couldn't match type ‘ab’ with ‘'(a0, b0)’ 
     ‘ab’ is a rigid type variable bound by 
     the type signature for: 
      backward :: forall (ab :: (*, *)). (forall a b. f '(a, b)) -> f ab 
     at :6:116 
     Expected type: f ab 
     Actual type: f '(a0, b0) 
    • In the expression: x 
     In an equation for ‘backward’: backward x = x

Понятно, что это действительно действующая программа. Есть ли другой способ реализовать эту функцию? Или это известное ограничение GHC?

источник

2016-09-06 Robert Hensing

Не уверен, что вычисление уровня уровня является подходящей меткой, когда «вычисление» на уровне типа не является целью. –

Насколько мне известно, и многое для моей досады, GHC еще не считает, что 'ab ~ '(Fst ab, Snd ab)', где 'Fst' и' Snd' являются проекциями уровня уровня , – pigworker

Dunno наверняка, но на догадку: ['Any'] (https://hackage.haskell.org/package/ghc-prim-0.5.0.0/docs/GHC-Prim.html#t:Any) снова наносит ответный удар , ('Any :: (*, *)', но это не тот случай, когда 'Any ~ (a, b)' для любых 'a' и' b'.) –

Проблема, как указывает свиновод и Даниэль Вагнер, заключается в том, что ab может быть «застрявшим» типом. Иногда вы можете обойти это с семьями типа (как я узнал в one of pigworker's papers):

type family Fst (x :: (k1, k2)) :: k1 where 
    Fst '(t1, t2) = t1 

type family Snd (x :: (k1, k2)) :: k2 where 
    Snd '(t1, t2) = t2 

backward :: forall (f :: (*, *) -> *) (ab :: (*, *)) proxy . 
      proxy ab -> 
      (forall (a :: *) (b :: *). f '(a, b)) -> 
      f '(Fst ab, Snd ab) 
backward _ x = x

Другой вариант, иногда, является использование оберток.

newtype Curry f x y = Curry (f '(x,y)) 

data Uncurry f xy where 
    Uncurry :: f x y -> f '(x, y)

источник

2016-09-06 18:46:24 dfeuer

Можно ли «разогнать» полный квантор?

ответ

Смежные вопросы