Отсутствие вывода типа приводит к неудачной компиляции, нет двусмысленности экземпляра - PullRequest
Новая
       33

Отсутствие вывода типа приводит к неудачной компиляции, нет двусмысленности экземпляра

5 голосов
/ 29 августа 2011

Я озадачен тем, почему этот код компилируется с подсказками типов, но не компилируется без. Не должно быть никаких неоднозначностей экземпляров (есть один экземпляр). 

class Monad m => FcnDef β m | β -> m where
    def :: String -> β -- takes a name

instance Monad m => FcnDef (m α -> m α) m where
    def s body = body

dummyTest :: forall m. Monad m => m ()
dummyTest = def "dummy" ((return ()) :: m ())

С другой стороны, если пропустить :: m () или все объявления типов, компиляция завершится с этой ошибкой, 

No instance for (FcnDef (m0 () -> t0) m0)
  arising from a use of `def'

Для пояснения код пытается создать многовариантный тип для def, поэтому можно написать, например, 

def "dummy2" "input" $ \in -> return ()

Редактировать

Этот вопрос более интересен, чем вопрос об отсутствии мономорфизма. Если добавить такой код, то разрешает экземпляры в конкретные типы, а именно 

dummyTest = def "dummy" (return ())
g :: IO ()
g = dummyTest

компиляция завершается аналогично.

Ответы [ 2 ]

7 голосов
/ 29 августа 2011

Необходимость подписи внешнего типа вызвана ограничением мономорфизма .

. Отдача для этого - левая часть вашего определения. 

dummyTest = ...

Поскольку это определение не имеет аргументов, компилятор попытается сделать это определение мономорфным.Добавление сигнатуры типа отменяет это поведение.

Однако, как вы указали, этого недостаточно.По какой-то причине компилятор не может определить тип внутреннего выражения.Зачем?Давайте разберемся.Пора играть в механизм вывода типов!

Давайте начнем с внешнего типа и попробуем определить тип внутреннего выражения. 

dummyTest :: forall m. Monad m => m ()
dummyTest = def "dummy" (return ())

Тип def равен FcnDef β m => String -> β, но здесь мы применили def к двум аргументам.Это говорит нам о том, что β должен быть типом функции.Давайте назовем это x -> y.

Затем мы можем легко сделать вывод, что y должно быть равно m (), чтобы удовлетворить внешний тип.Кроме того, тип аргумента return () равен Monad m1 => m1 (), поэтому мы можем сделать вывод, что искомый тип def должен иметь тип FcnDef (m1 () -> m ()) m0 => def :: String -> m1 () -> m ().

Далее мы продолжимискать экземпляр для использования.Единственный доступный экземпляр - , не достаточно универсальный , так как он требует, чтобы m1 и m были одинаковыми.Поэтому мы громко жалуемся на следующее сообщение: 

Could not deduce (FcnDef (m1 () -> m ()) m0)
  arising from a use of `def'
from the context (Monad m)
  bound by the type signature for dummyTest :: Monad m => m ()
  at FcnDef.hs:10:1-51
Possible fix:
  add (FcnDef (m1 () -> m ()) m0) to the context of
    the type signature for dummyTest :: Monad m => m ()
  or add an instance declaration for (FcnDef (m1 () -> m ()) m0)
In the expression: def "dummy" ((return ()))
In an equation for `dummyTest':
    dummyTest = def "dummy" ((return ()))

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

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

class Monad m => FcnDef β m | β -> m where
    def :: String -> β -> β

instance Monad m => FcnDef (m α) m where
    def s body = body

-- dummyTest :: forall m. Monad m => m ()
dummyTest = def "dummy" (return ())

Теперь механизм вывода типов может легкоопределите, что монада return должна совпадать с монадой в результате, и, используя NoMonomorphismRestriction, мы также можем удалить сигнатуру внешнего типа.

Конечно, я не уверен на 100%, чтоВы пытаетесь достичь этого, поэтому вам придется судить, имеет ли это смысл в контексте того, что вы пытаетесь сделать.

3 голосов
/ 30 августа 2011

Как отметил @pigworker в комментарии:

Вывод экземпляра является защитным по отношению к возможным будущим экземплярам.Похоже, у вашей головы экземпляра дважды одна и та же переменная.Он не сработает, если что-то еще не заставит эти типы быть одинаковыми.

Это действительно существенная проблема, и хотя подход @ hammar по добавлению дополнительного параметра, вероятно, является наиболее полезным решением,в таком случае мы можем сделать наблюдение, а затем искажать слабость механизма выбора экземпляра в нашу пользу.Для начала обратите внимание, что мы не можем написать два экземпляра, подобных этому: 

instance Monad m => FcnDef (m α -> m α) m where -- etc...
instance Monad m => FcnDef (m1 α -> m2 b) m3 where -- etc...

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

Учитывая, что первый экземпляр - это то, что мы хотим в этом случае, и что перекрытие означает, что мы никогда не сможем добавить второй экземплярво всяком случае, мы можем потянуть быстрый на GHC.Мы начнем с фактического написания второго , общего экземпляра, но затем мы добавим что-то в контекст (который проверяется только позже!), Который принудительно объединяет типы.Если вы включите TypeFamilies, вы можете использовать ~ с хорошим эффектом здесь и написать это: 

instance (m1 ~ m2, m2 ~ m3, a ~ b, Monad m) => FcnDef (m1 α -> m2 b) m3 where -- etc...

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

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

...