haskell Как избежать этого бесконечного вида? (Связанные данные и StateT)

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

s = AssocTyp (StateT s m) a

Интуиция относительно того, почему на самом деле это не проблема, состоит в том, что

AssocTyp (StateT s m) a = AssocTyp (StateT s' m) a

для всех s и s'. Однако компилятор недостаточно умен, чтобы понять это. Я читал, что в некоторых случаях можно использовать newtype, чтобы избежать бесконечных типов; как мне это сделать?

Вот минимизированный код для воспроизведения вопроса,

{-# LANGUAGE KindSignatures, TypeFamilies #-}

import Control.Monad.Trans.State

class MyMonad (m :: * -> *) where
    data AssocTyp m :: * -> *

instance MyMonad m => MyMonad (StateT s m) where
    data AssocTyp (StateT s m) a = StateTA (AssocTyp m a)

isAssocTyp :: Monad m => (AssocTyp m a) -> m ()
isAssocTyp x = return ()

x = do
    v <- get
    isAssocTyp (v)

associated-types typing typeclass infinite haskell
person gatoatigrado    schedule 26.03.2012    source источник

Ответы (2)


arrow_upward
3
arrow_downward

Я не уверен, чего вы пытаетесь достичь. Однако равенство, которое вы заявляете,

AssocTyp (StateT s m) a = AssocTyp (StateT s' m) a

неверно, потому что вы используете семейство данных, а не семейство типов. Компилируется следующий код:

{-# LANGUAGE KindSignatures, TypeFamilies #-}

import Control.Monad.Trans.State

class MyMonad (m :: * -> *) where
    type AssocTyp m :: * -> *

instance MyMonad m => MyMonad (StateT s m) where
    type AssocTyp (StateT s m) = AssocTyp m

isAssocTyp :: Monad m => (AssocTyp m a) -> m ()
isAssocTyp x = return ()

x :: Monad m => StateT (AssocTyp m a) m ()
x = do
    v <- get
    isAssocTyp v

Разница между семейством типов и семейством данных заключается в том, что семейства данных инъективны, что означает следующее утверждение, если DF является семейством данных:

DF a b c = DF a' b' c'   =====>     a = a',   b = b',   c = c'

В вашем случае это не то, что вам нужно.

person reinerp    schedule 26.03.2012
comment
ах, большое спасибо !! Мне кажется, я путаю равенство на уровне типов и данных. - person gatoatigrado; 27.03.2012

arrow_upward
0
arrow_downward

На всякий случай, если вам нужно семейство данных, у меня есть вариант, который выполняет проверку типа:

isAssocType' :: (Monad m1, Monad m0) => (AssocTyp m1 a) -> m0 ()
isAssocType' _ = return ()
person Chris Kuklewicz    schedule 26.03.2012
comment
Извините, isAssocType был уменьшен (для примера). - person gatoatigrado; 27.03.2012