Иметь это в обоих направлениях с ранг-н-типами - PullRequest
Новая
       65

Иметь это в обоих направлениях с ранг-н-типами

2 голосов
/ 20 апреля 2019

Я играю с монадой в стиле ConduitT, которая использует экзистенциальную квантификацию, и я играю в прятки, пытаясь объединить типы. Существует две версии этого сценария:

Здесь Await i имеет количественно экзистенциально a, что позволяет методу await передавать его в любой тип i -> Await i -> a, какой он пожелает. 

{-# LANGUAGE RankNTypes #-}

newtype Piped r a = Piped { unPiped :: forall b. r -> (r -> a -> b) -> b }

instance Functor (Piped r) where                              
  fmap f (Piped c) = Piped $ \r rest -> c r (\r -> rest r . f)

runPiped :: Piped r a -> r -> a      
runPiped (Piped p) r = p r $ \_ -> id

newtype Await i = Await { unAwait :: forall a. Yield i a -> a }           
newtype Yield i a = Yield { unYield :: i -> Await i -> a }                

runAwait :: Await i -> (i -> Await i -> a) -> a                           
runAwait (Await await) = await . Yield                                    

runYield :: Yield i a -> i -> (Yield i a -> a) -> a                       
runYield (Yield yield) i = yield i . Await
                     -- broke        ^^^^^
                     -- because Await swallows the type of `a`                                

await :: forall i a y. Piped (Await i, y) i                               
await = Piped $                                                           
  \(a, y) f -> runAwait a $ \i a' -> f (a', y) i

Сбой с: 

• Couldn't match type ‘Yield i a -> a’
                 with ‘forall a1. Yield i a1 -> a1’
  Expected type: (Yield i a -> a) -> Await i
    Actual type: (forall a. Yield i a -> a) -> Await i
• In the second argument of ‘(.)’, namely ‘Await’

Метод runYield не работает, поскольку он не может объединить экзистенциально определенный параметр типа в Await i с a.

Второй сценарий:

Для исправления runYield, Await теперь указывает a, который объединяет Await i a с Yield i a. Однако теперь, когда указано a, yield не может передать ему Yield i b с любым значением b, которое ему нравится: 

newtype Piped r a = Piped { unPiped :: forall b. r -> (r -> a -> b) -> b }
newtype Await i a = Await { unAwait :: Yield i a -> a }                   
newtype Yield i a = Yield { unYield :: i -> Await i a -> a }              

runAwait :: Await i a -> (i -> Await i a -> a) -> a                       
runAwait (Await await) = await . Yield                                    

runYield :: Yield i a -> i -> (Yield i a -> a) -> a                       
runYield (Yield yield) i = yield i . Await                                

await :: Piped (Await i a, y) i                                           
await = Piped $                                                           
  \(a, y) f -> runAwait a $ \i a' -> f (a', y) i                          
-- ^^^^^^

Сбой с: 

• Couldn't match type ‘b’ with ‘a’
  ‘b’ is a rigid type variable bound by
    a type expected by the context:
      forall b. (Await i a, y) -> ((Await i a, y) -> i -> b) -> b
  Expected type: (Await i a, y)
    Actual type: (Await i b, y)

Так что, мне кажется, мне это нужно в обоих направлениях, иногда количественно, а иногда - конкретно. Я пытался создать оболочки, чтобы скрыть дополнительный параметр типа, переключив newtype на data, и мне также пришло в голову, что если бы я мог определить функцию Await i a -> Await i b, которая также могла бы решить проблему, но я немного из моей глубины здесь. Есть идеи?

1 Ответ

0 голосов
/ 21 апреля 2019

Я столкнулся с той же проблемой, когда попытался определить функцию yield; мне пришлось удалить дополнительную переменную типа из yield, и она не проверяла бы тип.

Решение оказалось переопределить типы как таковые: 

newtype Await i = Await { unAwait :: forall b. Yield' i b -> b }     
newtype Yield i = Yield { unYield :: forall b. i -> Await' i b -> b }

type Await' i a = Yield i -> a                                       
type Yield' i a = i -> Await i -> a

Таким образом, в await нет дополнительного конструктора для глотания переменных типа: 

await :: Piped (Await i, y) i                  
await = Piped $                                
  \(Await a, y) f -> a $ \i a' -> f (a', y) i
...