• ? code Haskell typefun
    Помогите пожалуйста понять принцип работы 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, Так удобнее интересующимся: ideone.com
  • @qnikst, Я думал вчера задать этот вопрос в жуйке, но решил, что лучше дождаться пока ты спросишь. Больше шанс получить ответ :)
  • @balodja, Ну я отрекомендовал бы, думаю то же бы число тех, кто прочтет было б :)
  • @qnikst, GHC не может выбрать a, т.к. TF не инъективны о чём он и говорит
  • @qnikst, Я вроде про это написал в предположении? Просто если вроде тут указано, что 'a' тоже, что и в параметре, соотв ошибка должна переместиться в место вызова foo, где снова надо будет указывать тип. (Ну это работает при условии того, что FooE a b не вычисляется до последнего момента) или я не прав.
  • @qnikst, ну да. А вызвать foob вообще нельзя, так там всегда будет невыводимый тип a
  • @rkit, Я не спрашиваю как научить это работать, в прокси/дата family и я умею, я спрашиваю про логику работы type family и forall в данном контексте. :)
  • @qnikst, Логика очень простая — надо давать все типы в сигнатуру.
  • @rkit, foo :: forall a b. FooC a b => [FooE a b] -> [b] как бы все в сигнатуре есть. Смотри там в посте есть 3 вопроса, вот хорошо бы на них ответить или объяснить почему эти вопросы не важны, а важно что-то другое. На таком уровне я понимаю, но есть подозрение, что я упускаю что-то фундаментальное.
  • @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 :: [Char] -> Int, какой из инстансов foob будет применен внутри?
  • @rkit, В этом случае компилятор должен страшно ругаться в месте выбора foo и просить указать информацию (FooE B Int) там, например.
  • @qnikst, Он и будет ругаться. Там тоже надо параметр прикручивать
    foo :: FooC a b => a -> [FooE a b] -> [b]
    foo a = map (foob a)
  • @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 ?
  • @rkit, Я хочу вызывать

    foo' :: FooE A Int -> Int
    foo' = foo

    Например.

    И вопрос почему не тайпчекается foo, потому, что его не использовать? Почему тогда тайпчекается foob?
  • @qnikst, Наверно потому что можно написать хитрожопые инстансы вроде FooC a Int, где все должно работать. А может просто недосмотр.
  • @rkit, Возможно, ну я тогда пока буду продолжать верить, что ghc просто вычисляет FooE a b и получает какой-нить g ~ FooE a b, таким образом forall не связывает переменные a b и g. И думать над предложением про то, что возможно это из-за FooC a Int.
  • @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 может быть много.