Типовой семейный полиморфизм

Итак, у меня есть функция apply :: proxy tf -> tf Int -> tf Int, которая принимает прокси, предназначенный для передачи семейства типов, и применяет Int к этому семейству типов, чтобы определить тип второго аргумента и возвращаемого значения. Однако я получаю непонятные ответы от GHC.

{-# LANGUAGE TypeFamilies #-}

import Data.Proxy

type family F (a :: *) :: * where
    F Int = ()

f :: Proxy F
f = Proxy

apply :: proxy tf -> tf Int -> tf Int
apply _ x = x

-- Doesn't typecheck.
test1 :: ()
test1 = apply f ()

-- Typechecks fine
test2 :: ()
test2 = let g = apply f in g ()

test1 отказывается компилироваться с GHC, выдавая эту ошибку:

tftest.hs:16:9:
    Couldn't match expected type ‘()’ with actual type ‘F Int’
    In the expression: apply f ()
    In an equation for ‘test1’: test1 = apply f ()

tftest.hs:16:17:
    Couldn't match expected type ‘F Int’ with actual type ‘()’
    In the second argument of ‘apply’, namely ‘()’
    In the expression: apply f ()

Как ни странно, комментирование test1 и использование привязки let в test2 делает GHC счастливым, и все компилируется нормально. Кто-нибудь может объяснить, что здесь происходит?


polymorphism haskell type-families
person Nick Vladimiroff    schedule 24.04.2015    source источник

Ответы (1)


arrow_upward
12
arrow_downward

Итак, у меня есть функция apply :: proxy tf -> tf Int -> tf Int, которая принимает прокси, предназначенный для хранения семейства типов

Вы не можете этого сделать. Семейства типов всегда должны применяться полностью, как и синонимы типов, обобщением которых они являются. Переменная типа никогда не может быть создана для семейства типов с недостаточной насыщенностью.

Это ошибка в GHC 7.8.3, которая еще не отклоняла вашу программу, начиная с

f :: Proxy F
person Reid Barton    schedule 24.04.2015