GHC: ошибка в выводе параметра типа фантома - PullRequest
Новая
       31

GHC: ошибка в выводе параметра типа фантома

5 голосов
/ 17 января 2012

Итак, я пытаюсь создать тип для кортежей переменной длины, в основном как более симпатичные версии Either a (Either (a,b) (Either (a,b,c) ...)) и Either (Either (Either ... (x,y,z)) (y,z)) z. 

{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, FlexibleInstances #-}
module Temp where

-- type level addition
data Unit
data Succ n

class Summable n m where
  type Sum n m :: *

instance Summable Unit m where
  type Sum Unit m = Succ m

instance Summable n m => Summable (Succ n) m where
  type Sum (Succ n) m = Succ (Sum n m)

-- variable length tuple, left-to-right
data a :+ b = a :+ Maybe b
infixr 5 :+

class Prependable t r s where
  type Prepend t r s :: *
  prepend :: r -> Maybe s -> Prepend t r s

instance Prependable Unit x y where
  type Prepend Unit x y = x :+ y
  prepend = (:+)

instance Prependable n x y => Prependable (Succ n) (w :+ x) y where
  type Prepend (Succ n) (w :+ x) y = w :+ Prepend n x y
  prepend (w :+ Nothing) _ = w :+ Nothing
  prepend (w :+ Just x) y = w :+ Just (prepend x y)

-- variable length tuple, right-to-left
data a :- b = Maybe a :- b
infixl 5 :-

class Appendable t r s where
  type Append t r s :: *
  append :: Maybe r -> s -> Append t r s

instance Appendable Unit x y where
  type Append Unit x y = x :- y
  append = (:-)

instance Appendable n x y => Appendable (Succ n) x (y :- z) where
  type Append (Succ n) x (y :- z) = Append n x y :- z
  append _ (Nothing :- z) = Nothing :- z
  append x (Just y :- z) = Just (append x y) :- z

Однако компилятор, похоже, не может вывестипараметр фантомного типа prepend или append в рекурсивных случаях: 

Temp.hs:32:40:
    Could not deduce (Prepend t1 x y ~ Prepend n x y)
    from the context (Prependable n x y)
      bound by the instance declaration at Temp.hs:29:10-61
    NB: `Prepend' is a type function, and may not be injective
    In the return type of a call of `prepend'
    In the first argument of `Just', namely `(prepend x y)'
    In the second argument of `(:+)', namely `Just (prepend x y)'

Temp.hs:49:34:
    Could not deduce (Append t0 x y ~ Append n x y)
    from the context (Appendable n x y)
      bound by the instance declaration at Temp.hs:46:10-59
    NB: `Append' is a type function, and may not be injective
    In the return type of a call of `append'
    In the first argument of `Just', namely `(append x y)'
    In the first argument of `(:-)', namely `Just (append x y)'

Могу ли я что-нибудь сделать, чтобы помочь компилятору сделать этот вывод?

Ответы [ 2 ]

7 голосов
/ 17 января 2012

Важная часть сообщения об ошибке здесь: 

NB: `Prepend' is a type function, and may not be injective

Что это значит?Это означает, что может быть несколько instance Prependable, таких как type Prepend ... = a, так что если вы сделаете вывод Prepend как a, вы не обязательно будете знать, к какому экземпляру он принадлежит.

Вы можете решить эту проблему, используя типы данных в семействах типов , которые имеют преимущество в том, что вы не имеете дело с функциями типов, которые являются сюръективными, но может быть инъективными, и вместо этого с типом«отношения», которые являются биективными (поэтому каждый Prepend тип может принадлежать только одному семейству типов, а каждое семейство типов имеет отдельный Prepend тип).

(Если вы хотите, чтобы я показал решениес типами данных в семействах типов, оставьте комментарий! В основном, просто используйте data Prepend вместо type Prepend)

1 голос
/ 17 января 2012

Я решил добавить фиктивный аргумент для привязки prepend и append к фантомному параметру: 

-- as above, except...

unsucc :: Succ n -> n
unsucc _ = undefined

class Prependable t r s where
  type Prepend t r s :: *
  prepend :: t -> r -> Maybe s -> Prepend t r s

instance Prependable Unit x y where
  type Prepend Unit x y = x :+ y
  prepend _ = (:+)

instance Prependable n x y => Prependable (Succ n) (w :+ x) y where
  type Prepend (Succ n) (w :+ x) y = w :+ Prepend n x y
  prepend _ (w :+ Nothing) _ = w :+ Nothing
  prepend t (w :+ Just x) y = w :+ Just (prepend (unsucc t) x y)

class Appendable t r s where
  type Append t r s :: *
  append :: t -> Maybe r -> s -> Append t r s

instance Appendable Unit x y where
  type Append Unit x y = x :- y
  append _ = (:-)

instance Appendable n x y => Appendable (Succ n) x (y :- z) where
  type Append (Succ n) x (y :- z) = Append n x y :- z
  append _ _ (Nothing :- z) = Nothing :- z
  append t x (Just y :- z) = Just (append (unsucc t) x y) :- z
...