-
Помогите пожалуйста понять принцип работы forall с type families. Ниже минимальный пример неработающего кода, интересует метод foo. Особенно интересует то, что обозначает явное задание сигнатуры для foob в методе foo, с одной стороны FooE неинъективно и соотв компилятор не может выбрать конкретное foob, с другой a и b внесены под forall что должно быть подсказкой копилятору. Я так понимаю данное поведение зависит от следующего, FooE это функция из a b в элементы с kind *, соотвественно если на момент определения инстанса вместо FooE a b подставляется результат вычисления FooE a b, то получается то поведение, что мы видим (тип b финкирован результатом), а 'a' не определено. Если же редуцирования (?) не происходит, то тогда инстанс должен быть выбран. Соответсвенно вопросы: 1. правильны ли те предположения, что я написал выше 2. куда почитать, чтобы подтвердить их или опровергнуть 3. это баг или фича -- да, я знаю, что с data families все будет работать. {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE ScopedTypeVariables #-} class FooC a b where type FooE a b foob :: FooE a b -> b foo :: forall a b . FooC a b => [FooE a b] -> b foo = map (foob :: FooE a b -> b) вывод: 3.hs:9:8: Could not deduce (FooE a0 b ~ FooE a b) from the context (FooC a b) bound by the type signature for foo :: FooC a b => [FooE a b] -> b at 3.hs:9:8-47 NB: ‘FooE’ is a type function, and may not be injective The type variable ‘a0’ is ambiguous Expected type: [FooE a b] -> b Actual type: [FooE a0 b] -> b
♡ recommended by @balodja
Replies (19)
-
@qnikst, Я вроде про это написал в предположении? Просто если вроде тут указано, что 'a' тоже, что и в параметре, соотв ошибка должна переместиться в место вызова foo, где снова надо будет указывать тип. (Ну это работает при условии того, что FooE a b не вычисляется до последнего момента) или я не прав./5 · Reply
-
@qnikst, ну да. А вызвать foob вообще нельзя, так там всегда будет невыводимый тип a
-
@rkit, foo :: forall a b. FooC a b => [FooE a b] -> [b] как бы все в сигнатуре есть. Смотри там в посте есть 3 вопроса, вот хорошо бы на них ответить или объяснить почему эти вопросы не важны, а важно что-то другое. На таком уровне я понимаю, но есть подозрение, что я упускаю что-то фундаментальное.
-
@rkit, Там (в месте использования) его ругание вполне оправдано и понятно, потому прокся (доп параметр) нужна. Почему он требуется в foo мне не очевидно, т.е. я понимаю, что это из-за неиньективности, и того что FooE a b это не тип, а функция, но последовательно сложить это в вывод у меня не получается. Данные ответы на мой взгляд не отвечают на поставленный вопрос, или я где-то сильно туплю, во всяком случае я пока не увидел ничего, что я вчера не писал в чате, когда с этим разбирались ;)
-
@qnikst, instance FooC A Int where
type FooE A Int = Char
foob = 1
instance FooC B Int where
type FooE B Int = Char
foob = 2
foo :: forall a b. FooC a b => [FooE a b] -> [b]
foo = map (foob (undefined :: a))
вызываешь
foo :: [Char] -> Int
Каким будет undefined :: a ? -
@qnikst, Он не вычисляет какой-нибудь g, он при вызове foo "hello" прямо выводит FooE a b ~ String. Но этого просто недостаточно, чтобы найти a и b, чтобы передать их по forall., потому что функция неинъективна.
И случай с
foo' :: FooE A Int -> Int
foo' = foo
тоже не будет работать. Потому что FooE A Int это синоним. А синонимы в хаскеле не значат ничего, это все равно что #define FooE. Оно превратится в foo' :: String -> Int, а вариантов foo :: String -> Int может быть много.