Методы отслеживания ограничений

Вот сценарий: я написал некоторый код с сигнатурой типа, и жалобы GHC не смогли вывести x ~ y для некоторых xи y. Обычно вы можете бросить GHC кость и просто добавить изоморфизм в ограничения функции, но это плохая идея по нескольким причинам:

Это не подчеркивает понимание кода.
Вы можете получить 5 ограничений, которых было бы достаточно (например, если 5 подразумевает еще одно конкретное ограничение)
Вы можете получить фиктивные ограничения, если вы сделали что-то не так или если GHC бесполезен

Я потратил несколько часов на борьбу с делом 3. Я играю syntactic-2.0и пытаюсь определить независимую от домена версию share, аналогичную версии, определенной в NanoFeldspar.hs.

У меня было это:

{-# LANGUAGE GADTs, FlexibleContexts, TypeOperators #-}
import Data.Syntactic

-- Based on NanoFeldspar.hs
data Let a where
    Let :: Let (a :-> (a -> b) :-> Full b)

share :: (Let :<: sup,
          Domain a ~ sup,
          Domain b ~ sup,
          SyntacticN (a -> (a -> b) -> b) fi) 
      => a -> (a -> b) -> a
share = sugarSym Let

и GHC could not deduce (Internal a) ~ (Internal b), что, конечно, не то, что я собирался. Так что либо я написал какой-то код, который я не собирался (который требовал ограничения), либо GHC хотел это ограничение из-за некоторых других ограничений, которые я написал.

Оказывается, мне нужно было добавить (Syntactic a, Syntactic b, Syntactic (a->b))в список ограничений, ни один из которых не подразумевает (Internal a) ~ (Internal b). Я в основном наткнулся на правильные ограничения; У меня до сих пор нет систематического способа их найти.

Мои вопросы:

Почему GHC предложил это ограничение? Нигде в синтаксисе нет ограничений Internal a ~ Internal b, так откуда же GHC вытащил это?
В общем, какие методы можно использовать для отслеживания происхождения ограничения, в котором GHC считает это необходимым? Даже для ограничений, которые я могу обнаружить сам, мой подход заключается в грубой форсировке неправильного пути путем физического записи рекурсивных ограничений. Этот подход в основном сводится к бесконечной кроличьей норе ограничений и является наименее эффективным методом, который я могу себе представить.

haskell constraints ghc crockeea
источник

Были некоторые дискуссии об отладчике уровня типов, но общий консенсус, похоже, показывает, что внутренняя логика проверки типов не поможет: / На данный момент решатель ограничений Haskell - дерьмовый непрозрачный логический язык :)

Даниэль Гратцер

@jozefg У вас есть ссылка на это обсуждение?

crockeea

Часто это помогает просто полностью удалить сигнатуру типа и позволить ghci сказать вам, какой она должна быть.

Тобиас Брандт

Каким-то образом aи bсвязаны - посмотрите на сигнатуру типа вне вашего контекста - a -> (a -> b) -> aнет a -> (a -> b) -> b. Может это все? С помощью решателей ограничений они могут влиять на транзитивное равенство где угодно , но ошибки обычно показывают местоположение, «близкое» к тому, где было наложено ограничение. Это было бы здорово, хотя @jozefg - может быть, аннотировать ограничения с помощью тегов или чего-то еще, чтобы показать, откуда они пришли? : s

Атан Кларк

Прежде всего, ваша функция имеет неправильный тип; Я уверен, что так и должно быть (без контекста) a -> (a -> b) -> b. GHC 7.10 несколько более полезен для указания на это, потому что с вашим исходным кодом он жалуется на отсутствующее ограничение Internal (a -> b) ~ (Internal a -> Internal a). После исправления shareтипа GHC 7.10 помогает нам:

Could not deduce (Internal (a -> b) ~ (Internal a -> Internal b))
Добавив вышесказанное, получим Could not deduce (sup ~ Domain (a -> b))
После добавления этого мы получаем Could not deduce (Syntactic a), Could not deduce (Syntactic b)иCould not deduce (Syntactic (a -> b))

После добавления этих трех, он наконец проверяет тип; поэтому мы в конечном итоге

share :: (Let :<: sup,
          Domain a ~ sup,
          Domain b ~ sup,
          Domain (a -> b) ~ sup,
          Internal (a -> b) ~ (Internal a -> Internal b),
          Syntactic a, Syntactic b, Syntactic (a -> b),
          SyntacticN (a -> (a -> b) -> b) fi)
      => a -> (a -> b) -> b
share = sugarSym Let

Так что я бы сказал, что GHC не бесполезно ведет нас.

Что касается вашего вопроса о трассировке, откуда GHC получает свои требования к ограничениям, вы можете , в частности, попробовать отладочные флаги GHC-ddump-tc-trace , а затем прочитать итоговый журнал, чтобы увидеть, где Internal (a -> b) ~ tи (Internal a -> Internal a) ~ tдобавлены в Wantedнабор, но это будет довольно долгое чтение. ,

Кактус
источник

Методы отслеживания ограничений

Ответы: