2016-04-11 4 views
1

я был разочарован тем, что он правильно набрав:Haskell - почему он имеет правильные типы?

renumberTree2' :: Tree a -> StateT Int Identity (Tree Int) 
renumberTree2' t = get >>= (\v -> return (Empty)) 

В конце концов, у нас есть что:
(>>=) :: m a -> (a -> m b) -> m b. В связи с тем, что StateT s m a мы не можем дать привязать get :: StateT s m s. get не относится к типу m a как и ожидалось.
Однако get s, где s :: s->(a, s') - правильный тип, который должен быть привязан. Где я ошибаюсь?

ответ

6

Вы ошибаетесь при чтении типов. Вы можете обрабатывать более высокие типы типов (те, у которых есть параметры типа), так же, как и функции с приоритетом. Если у вас есть функция

f :: a -> b -> c -> d -> e 
f a b c d = undefined 

Затем назвав его

let e = f a b c d 

эквивалентно

let e = (((f a) b) c) d 

С f a :: b -> c -> d -> e, и так далее для (f a) b и т.д.

Когда вы видите тип StateT s m a, вы также можете прочитать его как ((StateT s) m) a, типы эквивалентны, и GHC с радостью примет этот синтаксис. Таким образом, это может быть проще, чтобы увидеть, как Monad m => StateT s m a могут быть приведены в соответствие с Monad m' => m' a':

m' ~ StateT s m 
a' ~ a 

Это означает, что Monad m' в вопросе StateT s m. Более простым примером, который работает точно так же, является пример Functor для Either a. Это не Either, у которого есть экземпляр Functor, но Either a, так как Functor является типом с видом * -> *, что означает тип, который принимает только один параметр типа.

+0

Мне казалось, что у монады всегда есть тип, это не означает 'm', всегда' m a' –

+0

@HaskellFun Я думаю, что вы на 80% понимаете это полностью. Вот несколько моментов для дальнейшего изучения. Только типы с типом '*' могут иметь значения. Любой тип, который вы ожидаете получить, например, тот, который отображается справа от '->', должен иметь вид '*'. Монады имеют вид '* -> *', что означает, что вы должны дать им аргумент вида '*' для получения типа вида '*' out. Тем не менее, вы все равно можете использовать свою монаду 'm' самостоятельно в выражениях другого типа, например' MonadTrans t => t m a'. –

2

В конце концов, мы имеем, что: (>>=) :: m a -> (a -> m b) -> m b

> :type (>>=) 
(>>=) :: Monad m => m a -> (a -> m b) -> m b 

True.

get не относится к типу m a как и ожидалось [by] bind.

> import Control.Monad.State 
> :type get 
get :: MonadState s m => m s 

Нет, get имеет тип m a (хотя он действительно несет ограничение).

1

get имеет тип m s, где s - государственный тип. MonadState экземпляра для StateT имеет контекст:

Monad m => MonadState s (StateT s m) 

поэтому тип монады m является StateT s m.Поэтому тип get для StateT является:

(StateT s m) s 

Функция дана (>>=) должна иметь тип s -> StateT s m b для некоторого результата типа b.

return (Empty) 

имеет тип StateT s m (Tree Int), как требуется, поскольку StateT s m является монадой.