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

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

7 голосов
/ 26 ноября 2011

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

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

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)

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

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

1 Ответ

9 голосов
/ 26 ноября 2011

Давайте сначала посмотрим на неудачные случаи. Оба они терпят неудачу по одной и той же причине, которая становится понятнее, когда вы добавляете неявное 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, но опять же, функция должна быть определена для any o1, поэтому мы не можем предположить, что o ~ o1.

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

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

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)

1 Попробуйте использовать let вместо case для забавная ошибка GHC :)

...