Могу ли я статически отклонять различные экземпляры экзистенциального типа?

Первая попытка

Сложно сделать этот вопрос содержательным, но для минимального примера предположим, что у меня есть такой тип:

{-# LANGUAGE GADTs #-}
data Val where
  Val :: Eq a => a -> Val

Этот тип позволяет мне с радостью составить следующий список, выглядящий неоднородно:

l = [Val 5, Val True, Val "Hello!"]

Но, увы, когда я записываю Eq экземпляр, все идет не так:

instance Eq Val where
  (Val x) == (Val y) = x == y -- type error

Ах, значит, мы Could not deduce (a1 ~ a). Совершенно верно; в определении ничего не сказано, что x и y должны быть одного типа. Фактически, все дело в том, чтобы допустить возможность их различий.

Вторая попытка

Давайте добавим Data.Typeable в микс и попробуем сравнить их только в том случае, если они одного типа:

data Val2 where
  Val2 :: (Eq a, Typeable a) => a -> Val2

instance Eq Val2 where
  (Val2 x) == (Val2 y) = fromMaybe False $ (==) x <$> cast y

Это очень мило. Если x и y одного типа, используется базовый экземпляр Eq. Если они отличаются, он просто возвращает False. Однако эта проверка откладывается до времени выполнения, что позволяет nonsense = Val2 True == Val2 "Hello" выполнить проверку типов без жалоб.

Вопрос

Я понимаю, что здесь я заигрываю с зависимыми типами, но возможно ли, чтобы система типов Haskell статически отклонила что-то вроде приведенного выше nonsense, позволяя при этом что-то вроде sensible = Val2 True == Val2 False возвращать False во время выполнения?

Чем больше я работаю над этой проблемой, тем больше мне кажется, что мне нужно применять некоторые методы HList для реализации необходимых мне операций как функций уровня типа. Однако я относительно новичок в использовании экзистенциалов и GADT, и мне любопытно узнать, можно ли найти решение именно с ними. Итак, если ответ отрицательный, я был бы очень признателен за обсуждение того, где именно эта проблема достигает предела этих функций, а также за подталкивание к подходящим методам, HList или другим.


haskell type-level-computation existential-type gadt
person acfoltzer    schedule 27.09.2011    source источник

Ответы (2)


arrow_upward
7
arrow_downward

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

Val True == Val "bar"  --> type error

allSame [] = True
allSame (x:xs) = all (== x) xs

allSame [Val True, Val "bar"]  --> False

Но обязательно:

(x == y) = allSame [x,y]

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

person luqui    schedule 27.09.2011
comment
Это очень показательный пример, поскольку он приближается к реальному приложению, которое я имею в виду, и показывает мне, как много я прошу здесь от системы типов. Есть ли у вас какие-либо мысли о том, подходит ли HList, если желаемое поведение состоит в том, чтобы статически отклонять что-то вроде этого примера вызова allSame? - person acfoltzer; 27.09.2011
comment
Да, именно для этого и предназначен HList. В свою очередь, работа со списками становится менее гибкой. Я считаю, что призывы к такому большому количеству уловок систем типов - это запах дизайна - Haskell наилучшим образом раскрывает простоту вашей проблемы. Но это личное предпочтение. - person luqui; 27.09.2011
comment
В самом деле, и это то, что я разделяю. Первый подход к полной проблеме, над которой я здесь решаюсь, - встраиванию языка логического программирования - будет восхитительно простым, если вы рассматриваете Val как стандартный тип суммы. Однако он закрыт для расширения и не предлагает статической проверки целесообразности унификации языка. Я работаю с syb, чтобы решить первую проблему, и этот вопрос - мой удар по второй. - person acfoltzer; 27.09.2011
comment
@acfoltzer, а, я понял. Я пытался сделать то же самое. Это сложно - возможно, поэтому Curry выделился на свой собственный язык. - person luqui; 27.09.2011

arrow_upward
14
arrow_downward

Чтобы принимать решения о проверке типов на основе содержащихся типов, нам необходимо «запомнить» содержащийся тип, выставив его как параметр типа.

data Val a where
  Val :: Eq a => a -> Val a

Теперь Val Int и Val Bool - это разные типы, поэтому мы можем легко обеспечить, чтобы разрешены только сравнения одного типа.

instance Eq (Val a) where
  (Val x) == (Val y) = x == y

Однако, поскольку Val Int и Val Bool - разные типы, мы не можем смешивать их вместе в списке без дополнительного уровня, который снова «забывает» содержащийся тип.

data AnyVal where
  AnyVal :: Val a -> AnyVal

-- For convenience
val :: Eq a => a -> AnyVal
val = AnyVal . Val

Теперь мы можем написать

[val 5, val True, val "Hello!"] :: [AnyVal]

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

person hammar    schedule 27.09.2011
comment
Очень полезно использовать слово «забывает» с AnyVal. К сожалению, это еще больше убеждает меня в том, что я слишком многого прошу от системы типов. По-видимому, мне нужен тип, который забывает достаточно долго, чтобы находиться в гетерогенной коллекции, но затем удобно запоминает, как только мне нужно знать содержащийся тип. - person acfoltzer; 27.09.2011