Экземпляр семейства типов Haskell с ограничениями типа

Я пытаюсь представить выражения с помощью семейств типов, но, похоже, не могу понять, как написать ограничения, которые мне нужны, и я начинаю чувствовать, что это просто невозможно. Вот мой код:

class Evaluable c where
    type Return c :: *
    evaluate :: c -> Return c

data Negate n = Negate n

instance (Evaluable n, Return n ~ Int) => Evaluable (Negate n) where
    type Return (Negate n) = Return n
    evaluate (Negate n) = negate (evaluate n)

Все это хорошо компилируется, но не выражает в точности того, что я хочу. В ограничениях Negate экземпляра Evaluable я говорю, что возвращаемый тип выражения внутри Negate должен быть Int (с Return n ~ Int), чтобы я мог вызвать отрицание для него, но это слишком ограничительно. На самом деле возвращаемый тип должен быть только экземпляром класса типа Num, который имеет функцию negate. Таким образом, Doubles, Integers или любой другой экземпляр Num также может быть инвертирован, а не только Ints. Но я не могу просто написать

Return n ~ Num

вместо этого, потому что Num - это класс типа, а Return n - это тип. Я тоже не могу поставить

Num (Return n)

вместо этого, потому что Return n - это тип, а не переменная типа.

Возможно ли то, что я пытаюсь сделать с Haskell? Если нет, так должно быть, или я неправильно понимаю какую-то теорию, стоящую за этим? Я чувствую, что Java могла бы добавить подобное ограничение. Дайте мне знать, если этот вопрос будет более ясным.

Изменить: Спасибо, ребята, ответы помогают и достигают того, о чем я подозревал. Похоже, что средство проверки типов не может справиться с тем, что я хотел бы сделать без UndecidableInstances, поэтому мой вопрос: действительно ли то, что я хотел бы выразить, действительно неразрешимо? Это для компилятора Haskell, но так ли вообще? т.е. может ли вообще существовать ограничение, которое означает «проверьте, что Return n является экземпляром Num», которое разрешается более продвинутой проверкой типов?


typeclass type-constraints haskell type-level-computation type-families
person user3773003    schedule 07.10.2015    source источник
comment
кстати, разве GHC никогда не рекомендовал расширение языка, например, FlexibleContexts или что-то еще в процессе проб и ошибок? потому что я совершенно уверен, что это так - небольшое примечание по возможно ли это даже с битом Haskell.   -  person Erik Kaplun    schedule 07.10.2015

Ответы (2)


arrow_upward
6
arrow_downward

Собственно, вы можете сделать именно то, что упомянули:

{-# LANGUAGE TypeFamilies, FlexibleContexts, UndecidableInstances #-}

class Evaluable c where
    type Return c :: *
    evaluate :: c -> Return c

data Negate n = Negate n

instance (Evaluable n, Num (Return n)) => Evaluable (Negate n) where
    type Return (Negate n) = Return n
    evaluate (Negate n) = negate (evaluate n)

Return n, безусловно, является типом, который может быть экземпляром класса точно так же, как Int. Ваше замешательство может заключаться в том, что может быть аргументом ограничения. Ответ: «все, что угодно, только в правильном виде». Тип Int - *, как и вид Return n. Num имеет вид * -> Constraint, поэтому что угодно * может быть его аргументом. Совершенно законно (хотя и бессмысленно) писать Num Int в качестве ограничения точно так же, как Num (a :: *).

person crockeea    schedule 07.10.2015
comment
Правильно, мне следовало объяснить, что я уже изучал это, но расширения FlexibleContexts и UndecidableInstances заставляют меня нервничать. Я чувствую, что они могут вернуться и укусить меня в конце, добавляя больше экземпляров, если я не ошибаюсь. - person user3773003; 07.10.2015
comment
Насколько мне известно, FlexibleContexts полностью безопасен и просто позволяет использовать переменные, не относящиеся к типу, в качестве параметров типа. UndecidableInstances может вызвать прерывание во время компиляции, если ваши экземпляры образуют цикл (поскольку компилятор не может это проверить). Для получения дополнительной информации см. этот ответ. - person crockeea; 07.10.2015
comment
@ user3773003: Я хочу сказать нечто более сильное, чем Эрик: я не думаю, что разумно использовать TypeFamilies без FlexibleContexts, и, вероятно, не без UndecidableInstances! Правила негибкого контекста были разработаны для языка без семейств типов; неудивительно, что им нужно продление. А поскольку семейства типов являются функциями уровня типа, неудивительно, что средство проверки завершения (уровня типа) может мешать, тем более что оно не очень умно; у нас нет средства проверки завершения на уровне значений, поэтому UndecidableInstances дает нам аналогичный уровень выразительности. - person Antal Spector-Zabusky; 07.10.2015
comment
@ user3773003 Я считаю FlaxibleContexts совершенно безвредным и надеюсь, что он будет включен в следующий стандарт Haskell. UndecidableInstances тоже в порядке, хотя я вижу некоторую ценность в том, чтобы включать его явно. Экземпляры OTOH, Incoherent- и Overlapping- являются злом, и их следует избегать как можно чаще. - person chi; 07.10.2015

arrow_upward
2
arrow_downward

Чтобы дополнить ответ Эрика, позвольте мне предложить одну возможную альтернативу: использование функциональной зависимости вместо семейства типов:

class EvaluableFD r c | c -> r where
  evaluate :: c -> r

data Negate n = Negate n

instance (EvaluableFD r n, Num r) => EvaluableFD r (Negate n) where
  evaluate (Negate n) = negate (evaluate n)

Думаю, это упрощает разговор о типе результата. Например, вы можете написать

foo :: EvaluableFD Int a => Negate a -> Int
foo x = evaluate x + 12

Вы также можете использовать ConstraintKinds, чтобы применить это частично (поэтому я помещаю аргументы в таком забавном порядке):

type GivesInt = EvaluableFD Int

Вы можете сделать это и со своим классом, но это будет раздражать больше:

type GivesInt x = (Evaluable x, Result x ~ Int)
person dfeuer    schedule 07.10.2015
comment
Да, снова то, что я должен был упомянуть, что я пробовал в исходном вопросе. Для этого тоже нужны UndecidableInstances, а также FlexibleInstances, которых я бы хотел избежать. - person user3773003; 07.10.2015
comment
@ user3773003, я не слишком оптимистичен, что вы можете получить то, что хотите, без этих расширений. Конечно, я мог что-то упустить. - person dfeuer; 07.10.2015
comment
@ user3773003 У FlexibleInstances нет недостатков буквально, и UndecidableInstances также эффективно безвреден. - person András Kovács; 07.10.2015
comment
@ AndrásKovács, Экметт предпочитает избегать гибких экземпляров, когда это возможно (я думаю, чтобы улучшить разрешение экземпляров), но только когда это возможно. - person dfeuer; 07.10.2015