haskell - не понимая, почему этому примеру связанного типа нужно больше выводов - PullRequest
Новая
       24

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

0 голосов
/ 12 сентября 2011

Рассмотрим следующий код: 

data MyBaseExpr α where
    ConstE :: Show α => α -> MyBaseExpr α

class Monad ? => MyMonadCls ? where
    type ExprTyp ? :: * -> *
    var :: String -> ExprTyp ? α -> ? (ExprTyp ? α)

expTypArg :: forall ? α. MyMonadCls ? => ExprTyp ? α -> ? α
expTypArg a = undefined

-- dummy type which will be used as an instance
newtype A ? α = A (? α)

Затем, если кто-то пытается написать экземпляр, используя функцию expTypeArg, 

instance forall ?. (Monad ?, Monad (A ?)) => MyMonadCls (A ?) where
    type ExprTyp (A ?) = MyBaseExpr
    var nme init@(expTypArg -> typb) =
        return init

компилятор жалуется 

Couldn't match type `ExprTyp ?0' with `MyBaseExpr'
Expected type: ExprTyp (A ?) α
  Actual type: ExprTyp ?0 α

Но, если добавить несколько выражений типа scoped, 

instance forall ?. (Monad ?, Monad (A ?)) => MyMonadCls (A ?) where
    type ExprTyp (A ?) = MyBaseExpr
    var nme init@((expTypArg :: MyMonadCls (A ?) =>
                   ExprTyp (A ?) α ->
                   (A ? α)) -> typb) =
        return init

, то это разрешится нормально.Что за проблема решается ExprTyp == MyBaseExpr для expTypArg?

edit

Большое спасибо, Даниэль!Вот способ убрать некоторые из пустяков, заметив, что нужно применять только тип ?. 

ignore_comp :: ? α -> ? β -> ? β
ignore_comp a b = b

instance forall ?. (Monad ?, Monad (A ?)) => MyMonadCls (A ?) where
    type ExprTyp (A ?) = MyBaseExpr
    var nme init@(expTypArg -> typb) =
        typb `ignore_comp`
        return init

1 Ответ

3 голосов
/ 12 сентября 2011

ExprTyp не является (обязательно) функцией инъективного типа. Это означает, что при передаче чего-то типа ExprType m не получается m - также может быть другой n такой, что ExprType n = ExprType m. Это делает тип expTypArg немного хитрым: он использует полиморфизм возвращаемого типа таким же образом, как, например, read, так что вам нужно будет добавить дополнительные аннотации типа к его результату в тех же ситуациях, что и вам. делать с read.

...