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

322

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

  1. Это не подчеркивает понимание кода.
  2. Вы можете получить 5 ограничений, которых было бы достаточно (например, если 5 подразумевает еще одно конкретное ограничение)
  3. Вы можете получить фиктивные ограничения, если вы сделали что-то не так или если 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). Я в основном наткнулся на правильные ограничения; У меня до сих пор нет систематического способа их найти.

Мои вопросы:

  1. Почему GHC предложил это ограничение? Нигде в синтаксисе нет ограничений Internal a ~ Internal b, так откуда же GHC вытащил это?
  2. В общем, какие методы можно использовать для отслеживания происхождения ограничения, в котором GHC считает это необходимым? Даже для ограничений, которые я могу обнаружить сам, мой подход заключается в грубой форсировке неправильного пути путем физического записи рекурсивных ограничений. Этот подход в основном сводится к бесконечной кроличьей норе ограничений и является наименее эффективным методом, который я могу себе представить.
crockeea
источник
21
Были некоторые дискуссии об отладчике уровня типов, но общий консенсус, похоже, показывает, что внутренняя логика проверки типов не поможет: / На данный момент решатель ограничений Haskell - дерьмовый непрозрачный логический язык :)
Даниэль Гратцер
12
@jozefg У вас есть ссылка на это обсуждение?
crockeea
36
Часто это помогает просто полностью удалить сигнатуру типа и позволить ghci сказать вам, какой она должна быть.
Тобиас Брандт
12
Каким-то образом aи bсвязаны - посмотрите на сигнатуру типа вне вашего контекста - a -> (a -> b) -> aнет a -> (a -> b) -> b. Может это все? С помощью решателей ограничений они могут влиять на транзитивное равенство где угодно , но ошибки обычно показывают местоположение, «близкое» к тому, где было наложено ограничение. Это было бы здорово, хотя @jozefg - может быть, аннотировать ограничения с помощью тегов или чего-то еще, чтобы показать, откуда они пришли? : s
Атан Кларк

Ответы:

6

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

  1. Could not deduce (Internal (a -> b) ~ (Internal a -> Internal b))

  2. Добавив вышесказанное, получим Could not deduce (sup ~ Domain (a -> b))

  3. После добавления этого мы получаем Could not deduce (Syntactic a), Could not deduce (Syntactic b)иCould not deduce (Syntactic (a -> b))

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

    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набор, но это будет довольно долгое чтение. ,

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

Вы пробовали это в GHC 8.8+?

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

Ключ должен использовать дыру типа среди ограничений: _ => your difficult type

Михал Гайда
источник