Типовая абстракция в GHC Haskell - PullRequest
Новая
       22

Типовая абстракция в GHC Haskell

0 голосов
/ 03 мая 2018

Я бы хотел получить следующий пример для проверки типов: 

{-# LANGUAGE AllowAmbiguousTypes    #-}
{-# LANGUAGE RankNTypes             #-}
{-# LANGUAGE TypeApplications       #-}
{-# LANGUAGE TypeFamilies           #-}

module Foo where

f :: Int -> (forall f. Functor f => Secret f) -> Int
f x _ = x

g :: (forall f. Functor f => Secret f) -> Int
g = f 4

type family Secret (f :: * -> *) :: * where
  Secret f = Int

Я понял, что, вероятно, невозможно вывести и проверить тип g (хотя в данном конкретном случае это очевидно, потому что это только частичное применение): Secret не является инъективным и нет способа сообщить компилятор, который Functor экземпляр должен ожидать. Следовательно, происходит сбой со следующим сообщением об ошибке: 

    • Could not deduce (Functor f0)
      from the context: Functor f
        bound by a type expected by the context:
                  forall (f :: * -> *). Functor f => Secret f
        at src/Datafix/Description.hs:233:5-7
      The type variable ‘f0’ is ambiguous
      These potential instances exist:
        instance Functor IO -- Defined in ‘GHC.Base’
        instance Functor Maybe -- Defined in ‘GHC.Base’
        instance Functor ((,) a) -- Defined in ‘GHC.Base’
        ...plus one other
        ...plus 9 instances involving out-of-scope types
        (use -fprint-potential-instances to see them all)
    • In the expression: f 4
      In an equation for ‘g’: g = f 4
    |
233 | g = f 4
    |     ^^^

Так что какое-то руководство от программиста необходимо, и оно с готовностью будет принято, если бы я мог написать g так: 

g :: (forall f. Functor f => Secret f) -> Int
g h = f 4 (\\f -> h @f)

Где \\ - это гипотетический синтаксис для большой лямбды в System Fw, то есть абстракция типа. Я могу эмулировать это с помощью уродливых Proxy s, но есть ли какая-то другая особенность GHC Haskell, которая позволяет мне писать что-то подобное?

Ответы [ 2 ]

0 голосов
/ 10 мая 2018

Это по замыслу. Кажется, сейчас нет никакого способа использовать Proxy s: https://ghc.haskell.org/trac/ghc/ticket/15119.

Редактировать июль 2019 года. Теперь есть предложение GHC для этого !

0 голосов
/ 03 мая 2018

Это может быть ошибка GHC. Я не могу понять, как это поведение GHC имеет какой-либо смысл.

Эта проблема не имеет ничего общего с семействами типов, но, похоже, она возникает из-за неоднозначных ограничений типов и типов.

Вот MCVE для той же проблемы. 

{-# LANGUAGE AllowAmbiguousTypes    #-}
{-# LANGUAGE RankNTypes             #-}
{-# LANGUAGE TypeApplications       #-}

class C a where
   getInt :: Int

instance C Char where
   getInt = 42

f :: (forall a. C a => Int) -> Bool
f x = even (x @ Char)

g :: (forall a. C a => Int) -> Bool
-- g = f               -- fails
-- g h = f h           -- fails
-- g h = f getInt      -- fails
g _ = f 42             -- OK

Похоже, что f нельзя вызвать ни с одним аргументом, который фактически использует ограничение.

...