Вывод ограничений как для if, так и для else равенства типов

Я пытаюсь заполнить дыру в следующем фрагменте

import Data.Proxy
import GHC.TypeLits
import Data.Type.Equality
import Data.Type.Bool
import Unsafe.Coerce

ifThenElse :: forall (a :: Nat) (b :: Nat) x l r.
  (KnownNat a, KnownNat b, x ~ If (a==b) l r) =>
  Proxy a -> Proxy b -> Either (x :~: l) (x :~: r)
ifThenElse pa pb = case sameNat pa pb of
  Just Refl -> Left Refl
  Nothing -> Right $ unsafeCoerce Refl -- This was the hole

Является ли это возможным?

Изменить: проверен источник sameNat< /a> и оказалось, что они используют unsafeCoerce. Я отредактировал код выше соответственно.


haskell dependent-type type-families
person fakedrake    schedule 15.02.2017    source источник
comment
Вероятно, вам следует опубликовать свое редактирование в качестве ответа (и отменить редактирование).   -  person Alec    schedule 15.02.2017
comment
Общая проблема, по-видимому, заключается в том, что, хотя сопоставление с образцом GADT обеспечивает ограничения равенства, оно никогда не обеспечивает ограничения неравенства, поэтому мы не можем убедить GHC в том, что первое предложение семейства закрытых типов не используется. Нам, вероятно, потребуется больше поддержки со стороны GHC, чтобы сделать это в будущем, AFAICS.   -  person chi    schedule 15.02.2017
comment
Тьфу, вы можете сказать, просто взглянув на тип, что это будет нелегко доказать, даже с индуктивным Nat (а не сломанным в GHC.TypeLits). Как вам удалось загнать себя в этот конкретный угол? Возможно, мы сможем посоветовать вам, как переделать вашу программу, чтобы вам не требовались такие корявые доказательства.   -  person Benjamin Hodgson♦    schedule 15.02.2017
comment
@BenjaminHodgson Я переписывал это снова и снова в течение нескольких дней, поэтому предложения действительно приветствуются. Я создаю класс типов Generic1, который должен иметь структуру E s = E0 s | E1 O1 (E s) | E2 O2 (E s) | .... Я реализовал различные общие функции, поэтому, похоже, он работает. Мне нужен безопасный способ извлечь Oi из заданной арности i безопасным способом. Итак (для некоторого понятия i :: Nat) getOp :: Proxy i -> e s -> Maybe (OpType i e). Поскольку i известен во время компиляции, GHC может (и делает) сделать вывод о точном типе приведенной выше подписи на каждом сайте вызова.   -  person fakedrake    schedule 15.02.2017
comment
@BenjaminHodgson, так вот в чем проблема: мне нужно пройти по дереву с уровнем типа Nat (который можно легко преобразовать из арности в глубину дерева), потому что GHC должен иметь возможность проверять тип каждого шага, поэтому мне нужно сказать ей (я вижу это как мать фиуре) как разобраться в типах.   -  person fakedrake    schedule 15.02.2017
comment
@BenjaminHodgson Суть проблемы заключается в обходе (примерно) (Op :*: recur) :+: rest, тип которого получен из If (c==n) Op (OpType' (c+1) n rest). c — текущая глубина, n — целевая глубина, я отслеживаю n и увеличиваю c вместо уменьшения n, потому что мне удобнее увеличивать, чем уменьшать понятие натуральных чисел GHC. В случае c==n GHC может выяснить, что это тип Op, и проверить все типы. В противном случае она не может доказать, что c==n и жалуется на проверку типов.   -  person fakedrake    schedule 15.02.2017
comment
Возможно, мне следует отредактировать вопрос со всей этой информацией, но я думаю, что контекст не имеет решающего значения для самого вопроса.   -  person fakedrake    schedule 15.02.2017

Ответы (1)


arrow_upward
2
arrow_downward

Одним из возможных решений является использование библиотеки singletons для получения функций уровня терминов, представляющих уровень типов. те (или наоборот).

Суть в следующем:

import Data.Singletons.Prelude

(...)

case (sing :: Sing a) %:== (sing :: Sing b) of
  STrue  -> Left Refl
  SFalse -> Right Refl

Я разместил автономный файл со всеми импортируемыми и языковыми расширениями.

person gallais    schedule 15.02.2017
comment
Большое спасибо! %:== не задокументирован? Я не могу найти это. - person fakedrake; 15.02.2017
comment
Data.Singletons.Prelude реэкспортирует Data.Singletons.Prelude.Eq, где можно найти (%:==) - person gallais; 15.02.2017