Как эта-редукция хорошо типизированной функции может привести к ошибке типа?

Я экспериментировал с линзами ван Лаарховена и столкнулся с проблемой, когда проверка типов отклоняла форму с сокращенным значением эта хорошо типизированной функции:

{-# LANGUAGE RankNTypes #-}

import Control.Applicative

type Lens c a = forall f . Functor f => (a -> f a) -> (c -> f c)

getWith :: (a -> b) -> ((a -> Const b a) -> (c -> Const b c)) -> (c -> b)
getWith f l = getConst . l (Const . f)

get :: Lens c a -> c -> a
get lens = getWith id lens

Вышеупомянутые проверки типов, но если я уменьшу get до

get :: Lens c a -> c -> a
get = getWith id

Тогда GHC (7.4.2) жалуется, что

Couldn't match expected type `Lens c a'
            with actual type `(a0 -> Const b0 a0) -> c0 -> Const b0 c0'
Expected type: Lens c a -> c -> a
  Actual type: ((a0 -> Const b0 a0) -> c0 -> Const b0 c0)
               -> c0 -> b0
In the return type of a call of `getWith'
In the expression: getWith id

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

Что заставляет GHC отвергать форму с сокращенным числом этажей и является ли это ошибкой / ограничением в GHC или какой-то фундаментальной проблемой с типами более высокого ранга?


haskell higher-rank-types
person shang    schedule 06.05.2013    source источник
comment
Имеет ли значение, когда вы пишете расширенный тип Lens?   -  person Ingo    schedule 07.05.2013

Ответы (2)


arrow_upward
12
arrow_downward

Я бы сказал, что причина не в самом η-сокращении, проблема в том, что с RankNTypes вы теряете основные типы и вывод типа.

Проблема с выводом типа с рангами более высокого порядка заключается в том, что вывод типа λx.M для подчинения правилу

     Γ, x:σ |- M:ρ
----------------------
  Γ |- λx:σ.M : σ→ρ

мы не знаем, какой тип σ выбрать для x. В случае системы типов Хиндли-Милнера мы ограничиваемся типами без кванторов для x, и вывод возможен, но не с произвольными ранжированными типами.

Таким образом, даже с RankNTypes, когда компилятор встречает термин без явной информации о типе, он обращается к Хиндли-Милнеру и выводит его основной тип ранга-1. Однако в вашем случае тип, который вам нужен для getWith id, - это ранг-2, и поэтому компилятор не может вывести его самостоятельно.

Ваш явный случай

get lens = getWith id lens

соответствует ситуации, когда тип x уже указан явно λ(x:σ).Mx. Компилятор знает тип lens перед проверкой типа getWith id lens.

В редуцированном случае

get = getWith id

компилятор должен сам вывести тип getWidth id, поэтому он придерживается Хиндли-Милнера и выводит неадекватный тип ранга-1.

person Petr    schedule 06.05.2013

arrow_upward
5
arrow_downward

На самом деле это довольно просто: GHC определяет типы для каждого выражения, а затем начинает объединять их по =. Это всегда хорошо работает, когда есть только типы ранга 1, потому что выбирается наиболее полиморфный (это четко определено); так что любое объединение, которое вообще возможно, будет успешным.

Но он не выберет более общий тип ранга 2, даже если это будет возможно, поэтому getWith id предполагается ((a -> Const a a) -> c -> Const a c) -> (c -> a), а не (forall f . Functor f => (a -> f a) -> c -> f c) -> (c -> a). Я полагаю, если бы GHC делал такие вещи, традиционный вывод типа ранга 1 вообще не работал бы. Или он просто никогда не завершился бы, потому что не существует одного четко определенного наиболее полиморфного типа rank-n.

Это не объясняет, почему он не видит из подписи get, что ему необходимо выбрать здесь ранг 2, но, по-видимому, для этого также есть веская причина.

person leftaroundabout    schedule 06.05.2013