Как haskell разрешает дублирование экземпляров? - программирование
Подтвердить что ты не робот

Как haskell разрешает дублирование экземпляров?

Пожалуйста, извините меня, если я использую неправильную терминологию, я много начинаю в манипуляции типа haskell... Я пытаюсь использовать перекрывающиеся экземпляры с функциональными зависимостями для программирования на уровне типа с помощью HLists.

Здесь моя цель - попытаться написать typeclass HNoNils l l', где HNoNils l l' означает, что при l, являющемся типом списка (ex: Int : String : EmptyNil : Int : HNil), l' - это соответствующий тип списка без конкретный пустой тип EmptyNil (результат примера: Int:String:Int:HNil):

{-# LANGUAGE ExistentialQuantification,
  FunctionalDependencies,
  FlexibleInstances,
  UndecidableInstances,
  OverlappingInstances,
  TypeFamilies #-}

import Data.HList 
import Data.TypeLevel.Bool

--Type Equality operators
--usedto check if a type is equal to another
class TtEq a b eq | a b -> eq
instance     TtEq a a True
instance eq~False => TtEq a b eq 


data EmptyNil = EmptyNil deriving (Show) --class representing empty channel
--class intended to generate a list type with no type of EmptyNil
-- Example: HCons Int $ HCons EmptyNil HNil should give HCons Int HNil
class (HList list, HList out) => HNoNils list out | list -> out 
    where  hNoNils :: list -> out 

-- l gives l' means (HCons EmptyNil l) gives l'
instance (HNoNils l l',TtEq e EmptyNil True ) => HNoNils (HCons e l) l'
    where hNoNils (HCons e l) = hNoNils l

-- l gives l' means (HCons e l) gives (HCons e l') for all e 
instance (HNoNils l l') => HNoNils (HCons e l) (HCons e l')
    where hNoNils (HCons e l) = hCons e $ hNoNils l

--base case
instance  HNoNils HNil HNil
    where hNoNils _ = hNil

testList  = HCons EmptyNil $ HCons EmptyNil HNil
testList1 = HCons "Hello"  $ HCons EmptyNil HNil 
testList2 = HCons EmptyNil $ HCons "World"  HNil
testList3 = HCons "Hello"  $ HCons "World"  HNil

main:: IO ()
main = do
    print $ hNoNils testList  -- should get HNil
    print $ hNoNils testList1 -- should get HCons "Hello" HNil
    print $ hNoNils testList2 -- should get HCons "World" HNil
    print $ hNoNils testList3 -- should get HCons "Hello" (HCons "World" HNil)

Однако, когда я запускаю этот код как есть, все мои вызовы hNoNils, кажется, разрешаются через наименьшее конкретное, второе объявление экземпляра, что означает (по крайней мере, похоже), что для всех l у меня есть HNoNils l l.

Основываясь на том, что я прочитал, с расширением OverlappingInstances, система должна всегда разрешать наиболее конкретный экземпляр.

Здесь

  • первый экземпляр имеет ограничения (HNoNils l l',TtEq e EmptyNil True )

  • второй экземпляр имеет ограничения HNoNils l l'

Простите меня, если я ошибаюсь, но похоже, что первый экземпляр более специфичен, чем второй, поэтому он должен идти за этим, не так ли?

Я попытался добавить ограничения, чтобы попытаться избавиться от перекрытия, а именно, добавив отдельное ограничение oposite равенства ко второму экземпляру:

-- l gives l' means (HCons EmptyNil l) gives l'
instance (HNoNils l l',TtEq e EmptyNil True ) => HNoNils (HCons e l) l'
    where hNoNils (HCons e l) = hNoNils l

-- l gives l' means (HCons e l) gives (HCons e l') for all e 
-- added constraint of TtEq e EmptyNil False
instance (HNoNils l l',TtEq e EmptyNil False) => HNoNils (HCons e l) (HCons e l')
    where hNoNils (HCons e l) = hCons e $ hNoNils l

Я попытался удалить перекрывающееся расширение экземпляра здесь, и я получаю ошибки перекрытия.

Overlapping instances for HNoNils
                                (HCons EmptyNil (HCons [Char] HNil)) (HCons EmptyNil l')
Matching instances:
      instance (HNoNils l l', TtEq e EmptyNil True) =>
               HNoNils (HCons e l) l'
        -- Defined at /home/raphael/Dropbox/IST/AFRP/arrow.hs:32:10
      instance (HNoNils l l', TtEq e EmptyNil False) =>
               HNoNils (HCons e l) (HCons e l')
        -- Defined at /home/raphael/Dropbox/IST/AFRP/arrow.hs:36:10

Я не понимаю второго матча. В конце концов, в этой резолюции мы имеем e равным EmptyNil, поэтому TtEq e EmptyNil True... right? И в этом отношении, как система типов даже попадает в ситуацию, когда она задает этот вопрос, ведь с ограничениями у вас никогда не должно быть ситуации типа HNoNils (Hcons EmptyNil l) (HCons EmptyNil l')), по крайней мере, я так не думаю.

При добавлении обратно OverlappingInstances, я получаю еще более странные ошибки, которые я не понимаю:

 Couldn't match type `True' with `False'
    When using functional dependencies to combine
      TtEq a a True,
        arising from the dependency `a b -> eq'
        in the instance declaration at /home/raphael/Dropbox/IST/AFRP/arrow.hs:23:14
      TtEq EmptyNil EmptyNil False,
        arising from a use of `hNoNils'
        at /home/raphael/Dropbox/IST/AFRP/arrow.hs:53:13-19
    In the second argument of `($)', namely `hNoNils testList2'
    In a stmt of a 'do' block: print $ hNoNils testList2

второй оператор TtEq EmptyNil EmptyNil False, кажется, говорит, что экземпляр был сгенерирован вызовом функции...? Я немного смущен относительно того, откуда он пришел.

Поэтому, пытаясь понять это, мне было интересно:

  • Можно ли получить более подробную информацию о том, как Haskell работает с экземплярами? Некоторые из этих комбинаций кажутся невозможными. Даже оценить связь с документом, объясняющим механизм, было бы оценено

  • Существует ли более конкретное определение того, как OverlappingInstances работает? Я чувствую, что мне что-то не хватает (например, аргумент "специфичность" работает только с переменными типа jthe, а не с количеством ограничений...)

edit. Поэтому я попробовал одно из предложений C.A. McCann (удаление некоторых ограничений) на следующее:

instance (HNoNils l l') => HNoNils (HCons EmptyNil l) l'

instance (HNoNils l l') => HNoNils (HCons e l) (HCons e l')

instance  HNoNils HNil HNil

Выполнение этого дает мне некоторые неприятные ошибки совпадающих экземпляров:

Overlapping instances for HNoNils
                                (HCons EmptyNil (HCons [Char] HNil)) (HCons EmptyNil l')
      arising from a use of `hNoNils'
    Matching instances:
      instance [overlap ok] HNoNils l l' => HNoNils (HCons EmptyNil l) l'
        -- Defined at /Users/raphael/Dropbox/IST/AFRP/arrow.hs:33:10
      instance [overlap ok] HNoNils l l' =>
                            HNoNils (HCons e l) (HCons e l')
        -- Defined at /Users/raphael/Dropbox/IST/AFRP/arrow.hs:37:10

Мне кажется, что метод разрешения сверху вниз, а не снизу вверх (где система никогда не попытается найти такой экземпляр).

edit 2: добавив небольшое ограничение ко второму условию, я получил ожидаемое поведение (см. комментарий Макканна о его ответе):

-- l gives l' means (HCons EmptyNil l) gives l'
instance (HNoNils l l') => HNoNils (HCons EmptyNil l) l'
    where hNoNils (HCons EmptyNil l) = hNoNils l

-- l gives l' means (HCons e l) gives (HCons e l') for all e 
instance (HNoNils l l',r~ HCons e l' ) => HNoNils (HCons e l) r
    where hNoNils (HCons e l) = hCons e $ hNoNils l

здесь добавленная вещь - это ограничение r~HCons e l' для второго экземпляра.

4b9b3361

ОТВЕТЫ

Ответ 1

Можно ли получить более подробную информацию о том, как Haskell работает с экземплярами? Некоторые из этих комбинаций кажутся невозможными. Было бы даже оценено даже ссылку на документ, объясняющий механизм.

Как работает Haskell с экземплярами очень просто. Вы имеете дело с несколькими расширениями экспериментального языка, предоставляемыми GHC, поэтому основным источником информации является Руководство пользователя GHC.

Существует ли более конкретное определение того, как работают OverlappingInstances? Я чувствую, что у меня что-то отсутствует (например, аргумент "специфичность" работает только с переменными типа jthe, а не с количеством ограничений...)

Ваша догадка правильная. Из раздела "Руководство пользователя" , объясняющего OverlappingInstances:

Когда GHC пытается разрешить, скажем, ограничение C Int Bool, он пытается сопоставить каждое объявление экземпляра с ограничением, создавая экземпляр главы объявления экземпляра. Например, рассмотрите эти объявления:

instance context1 => C Int a     where ...  -- (A)
instance context2 => C a   Bool  where ...  -- (B)
instance context3 => C Int [a]   where ...  -- (C)
instance context4 => C Int [Int] where ...  -- (D)

Экземпляры (A) и (B) соответствуют ограничению C Int Bool, но (C) и (D) этого не делают. При сопоставлении GHC не учитывает контекст объявления экземпляра (context1 и т.д.).

Подумайте об этом как о шаблонах против охранников:

instanceOfC Int a | context1 Int a = ...
instanceOfC a Bool | context2 a Bool = ...

Поскольку классы классов "открыты", не существует четко определенного порядка совпадений, как есть с функцией, поэтому вместо этого существуют ограничения на "шаблоны", которые соответствуют тем же аргументам. Я подробно остановился на аналогии с шаблонами и стражами в предыдущем ответе.

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

hNoNils (e:l) | e == EmptyNil = hNoNils l
hNoNils (e:l) = e : hNoNils l
hNoNils [] = []

Зная, что "охранники" игнорируются при выборе "шаблона", ясно, что первые два шаблона нельзя отличить.

Но я ожидаю, что вы хотели бы знать, как заставить все работать, а не просто, почему в настоящее время они этого не делают. (N.B. - У меня сейчас нет GHC, так что все это из памяти и не было проверено. Возможно, я получил несколько деталей.)

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

class FooConstraint a b r | a b -> r  -- some sort of type predicate


-- the "actual" type function we want
class (FooConstraint a b result, FooAux a b result c) => Foo a b c | a b -> c

-- a single maximally generic instance
instance (FooConstraint a b result, FooAux a b result c) => Foo a b c 


-- this class receives the original a and b as arguments, but also the 
-- output of the predicate FooConstraint
class FooAux a b result c | a b result -> c

-- which lets us indirectly choose instances based on a constraint
instance ( ... ) => FooAux a b True c 
-- more instances, &c.

Это огромная проблема, как вы можете видеть, но иногда все, что у вас есть.

К счастью, ваш случай намного проще. Напомним, что перевод на псевдофункцию выше - вы бы написали эту функцию таким образом? Конечно, нет, потому что это было бы яснее:

hNoNils (EmptyNil:l) = hNoNils l
hNoNils (e:l) = e : hNoNils l
hNoNils [] = []

Так как EmptyNil является конструктором, вы можете сопоставить его с шаблоном, упрощая код и избегая избыточного ограничения Eq.

То же самое относится к эквиваленту уровня: замените предикат равенства типа простым использованием EmptyNil в голове экземпляра:

instance (HNoNils l l') => HNoNils (HCons EmptyNil l) l'

instance (HNoNils l l') => HNoNils (HCons e l) (HCons e l')

instance  HNoNils HNil HNil

Эта версия по-прежнему будет работать в одной ситуации, и там действительно нет хорошего пути. Если список типов содержит переменные типа, которые могут потенциально объединяться с EmptyNil - имея в виду, что ограничения игнорируются на этом этапе и что GHC должен учитывать произвольные экземпляры, которые позднее добавляются для EmptyNil - первые два экземпляра неизбежно двусмысленны.

Проблемы неоднозначности этого последнего вида могут быть частично устранены путем обеспечения того, чтобы все соответствующие случаи можно было различать. Например, вместо удаления типа типа EmptyNil вы могли бы иметь конструкторы типов, например:

data Some a
data None

И затем напишите версию уровня catMaybes на уровне уровня:

class CatOptions l l'
instance (CatOptions l l') => CatOptions (HCons None l) l'
instance (CatOptions l l') => CatOptions (HCons (Some e) l) (HCons e l')
instance CatOptions HNil HNil

Это ограничивает проблемы двусмысленности только ситуациями, которые являются действительно двусмысленными, а не случаями, когда список содержит, например. полиморфный тип, представляющий произвольный экземпляр Num.