Ошибки типов с экзистенциальными типами в Haskell

Question

Я борюсь с экзистенциальными типами в моей программе. Я думаю, что пытаюсь сделать что-то очень разумное, однако я не могу пройти мимо проверки типов:(

У меня есть тип данных, который имитирует монаду

data M o = R o | forall o1. B (o1 -> M o) (M o1)

Теперь я создаю для него Контекст, аналогичный описанному в статье на Haskell Wiki о Zipper, однако для простоты я использую функцию вместо структуры данных -

type C o1 o2 = M o1 -> M o2

Теперь, когда я пытаюсь написать функцию, которая разделяет значение данных на контекст и подзначение, проверщик типов жалуется:

ctx :: M o -> (M o1 -> M o, M o1)
ctx (B f m) = (B f, m) -- Doesn't typecheck

Ошибка -

Couldn't match type `o2' with `o1'
  `o2' is a rigid type variable bound by
       a pattern with constructor
         B :: forall o o1. (o1 -> M o) -> M o1 -> M o,
       in an equation for `ctx'
       at delme1.hs:6:6
  `o1' is a rigid type variable bound by
       the type signature for ctx :: M o -> (M o1 -> M o, M o1)
       at delme1.hs:6:1
Expected type: M o2
  Actual type: M o1
In the expression: m
In the expression: (B f, m)

Тем не менее, я могу обойти это так -

ctx (B f m) = let (c,m') = ctx m in ((B f) . c, m') -- OK

Почему это второе определение проверяет тип, а не первое?

Кроме того, если я пытаюсь конвертировать ctx для полной функции, проверяя R, я снова получаю ошибку проверки типов -

ctx (R o) = (id, R o) -- Doesn't typecheck

Ошибка -

Couldn't match type `o' with `o1'
  `o' is a rigid type variable bound by
      the type signature for ctx :: M o -> (M o1 -> M o, M o1)
      at delme1.hs:7:1
  `o1' is a rigid type variable bound by
       the type signature for ctx :: M o -> (M o1 -> M o, M o1)
       at delme1.hs:7:1
In the first argument of `R', namely `o'
In the expression: R o
In the expression: (id, R o)

Как я могу обойти эту ошибку?

Любая помощь приветствуется!

Answer 1

Давайте сначала посмотрим на неудачные случаи. Оба из них терпят неудачу по одной и той же причине, которая становится понятнее, когда вы добавляете в неявное forall в подписи типа:

ctx :: forall o o1. M o -> (M o1 -> M o, M o1)

т.е. ваша функция должна работать не только для некоторых o1, но для любого o1,

1. В вашем первом случае,

   ctx (B f m) = (B f, m)
   

   мы знаем это f :: (o2 -> M o) а также m :: M o2 для какого-то типа o2, но мы должны быть в состоянии предложить любой тип o1 поэтому мы не можем предположить, что o1 ~ o2,

2. Во втором случае

   ctx (R o) = (id, R o)
   

   Здесь мы знаем, что o :: oно, опять же, функция должна быть определена для любого o1 поэтому мы не можем предположить, что o ~ o1,

Ваш обходной путь, кажется, работает только потому, что он вызывает сам себя, подобно индуктивному доказательству. Но без базового случая это просто циклическое рассуждение, и вы не можете написать базовый вариант для этой функции, потому что нет способа построить M o1 из M o для любой комбинации o а также o1 без использования нижнего значения.

Что вам, вероятно, понадобится, это определить другой экзистенциальный тип для контекста, вместо того, чтобы использовать просто кортеж. Не уверен, что это будет работать для ваших нужд, но это компилирует ¹, по крайней мере:

data Ctx o = forall o1. Ctx (M o1 -> M o) (M o1)

ctx :: M o -> Ctx o
ctx (B f m) = case ctx m of Ctx c m' -> Ctx (B f . c) m'
ctx (R o)   = Ctx id (R o) 

_{¹ Попробуйте использовать} let _вместо case _{за смешную ошибку GHC:)}