Проверка экземпляра класса типа не может обнаружить кусочные экземпляры

У меня есть семейство типов данных, проиндексированных целыми числами уровня типа, и я определяю их как экземпляры некоторого класса типов «кусочно», что вызывает проблемы при попытке получить экземпляры другого класса. Для иллюстрации я выделил проблему следующим образом. Рассмотрим этот код:

{-# LANGUAGE ScopedTypeVariables, TypeSynonymInstances,
             FlexibleInstances  , UndecidableInstances #-}

data Zero
data Succ n

type One   = Succ Zero
type Two   = Succ One
type Three = Succ Two

class Nat n where
  toInt :: n -> Int

instance Nat Zero where
  toInt _ = 0
instance Nat One where ------------------------- START MODIFY
  toInt _ = 1
instance (Nat n) => Nat (Succ (Succ n)) where
  toInt _ = 2 + toInt (undefined :: n) --------- END MODIFY

Это небольшая модификация целых чисел уровня типа, определенных в " Развлечения с функциями типов "Киселева, Джонса и Шаня. Компилируется нормально, и toInt, похоже, работает, как ожидалось. Прямо сейчас Nat содержит все целые числа Zero, One, Two и так далее.

Однако GHC жалуется после того, как я добавлю следующие строки и перекомпилирую:

class LikeInt n where
  likeInt :: n -> Int

instance (Nat n) => LikeInt (Succ n) where
  likeInt = toInt

Ошибка: не удалось вывести (Nat (Succ n)), возникшую в результате использования «toInt» из контекста (Nat n).

Я предполагаю, что когда GHC делает вывод, что toInt имеет аргумент типа Succ n, но единственные экземпляры для Nat - это Zero, Succ Zero и (Nat n0) => Succ (Succ n0), а Succ n не соответствует ни одному из них. Это предположение подтверждается успешной компиляцией, когда я заменяю блок MODIFY исходным

instance (Nat n) => Nat (Succ n) where
  toInt _ = 1 + toInt (undefined :: n)

Как мне заставить likeInt работать так же, как toInt, даже с измененным блоком? Это важно для моего настоящего проекта.


compiler-errors type-inference typeclass haskell type-families
person Herng Yi    schedule 17.07.2015    source источник
comment
Я хотел бы отметить здесь, что с современными функциями и библиотеками GHC (семейства закрытых типов, типы данных, одиночные экземпляры) у нас есть более мощные и удобные средства программирования на уровне типов, чем то, что представлено в цитируемой статье.   -  person András Kovács    schedule 17.07.2015
comment
Кроме того, почему у вас нет измененных экземпляров для Nat?   -  person András Kovács    schedule 17.07.2015
comment
Измененные экземпляры компилируются, но когда я пытаюсь получить экземпляры для LikeInt, это терпит неудачу.   -  person Herng Yi    schedule 18.07.2015

Ответы (2)


arrow_upward
0
arrow_downward

Разве вы не можете просто определить этот экземпляр?

instance Nat n => LikeInt n where
  likeInt = toInt

*Main> likeInt (undefined :: Zero)
0
*Main> likeInt (undefined :: One)
1
*Main> likeInt (undefined :: Two)
2
*Main> likeInt (undefined :: Three)
3

Или вы хотите избежать ограничения Nat?

person Nikita Karetnikov    schedule 17.07.2015
comment
Я намеренно определил LikeInt таким образом, чтобы показать несоответствие между логикой программиста и логикой компилятора. В моем реальном проекте мне нужны были экземпляры, определенные по-разному для разных подмножеств натуральных чисел, поэтому в этом случае вы могли бы сказать, что likeInt определен таким образом только для положительных целых чисел. - person Herng Yi; 18.07.2015

arrow_upward
0
arrow_downward

Компилятор сказал вам, что делать.

Ты имел

instance (Nat n) => LikeInt (Succ n) where
  likeInt = toInt

И компилятор сказал:

Could not deduce (Nat (Succ n)) arising from a use of ‘toInt’
from the context (Nat n)

Итак, мы меняем контекст, чтобы задать ограничение, о котором просил компилятор. Магия!

instance (Nat (Succ n)) => LikeInt (Succ n) where
  likeInt = toInt

(и это действительно компилируется).

person sclv    schedule 12.03.2016