Преобразование списка типов типов [a, b, c, ...] для функции a-> b-> c->

Question

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

{-# LANGUAGE KindSignatures, DataKinds, TypeOperators, 
      TypeFamilies, FlexibleInstances, PolyKinds #-} 

module Issue where 


type family (->>) (l :: [*]) (y :: *) :: * where 
    '[]  ->> y = y 
    (x ': xs) ->> y = x -> (xs ->> y) 

class CVal (f :: [*]) where 
    data Val f :: * 
    construct :: f ->> Val f 

instance CVal '[Int, Float, Bool] where 
    data Val '[Int, Float, Bool] = Val2 Int Float Bool 
    construct = Val2 

Это компилируется в порядке. Но когда я пытаюсь применить construct функцию:

v :: Val '[Int, Float, Bool] 
v = construct 0 0 True 

он производит ошибку:

Couldn't match expected type `a0 
           -> a1 -> Bool -> Val '[Int, Float, Bool]' 
      with actual type `f0 ->> Val f0' 
The type variables `f0', `a0', `a1' are ambiguous 
The function `construct' is applied to three arguments, 
but its type `f0 ->> Val f0' has none 
In the expression: construct 0 0 True 
In an equation for `v': v = construct 0 0 True 

Answer 1

Ваш код не в typecheck потому type families are not (necessarily) injective. Если вы помочь GHC, указав выбор f в f ->> Val f, то он работает, как ожидалось:

{-# LANGUAGE KindSignatures, DataKinds, TypeOperators, 
      TypeFamilies, FlexibleInstances, PolyKinds #-} 

module Issue where 

import Data.Proxy 

type family (->>) (l :: [*]) (y :: *) :: * where 
    '[]  ->> y = y 
    (x ': xs) ->> y = x -> (xs ->> y) 

class CVal (f :: [*]) where 
    data Val f :: * 
    construct :: proxy f -> f ->> Val f 

instance CVal '[Int, Float, Bool] where 
    data Val '[Int, Float, Bool] = Val2 Int Float Bool deriving Show 
    construct _ = Val2 

v :: Val '[Int, Float, Bool] 
v = construct (Proxy :: Proxy '[Int, Float, Bool]) 0 0 True 

Ключевой момент проходит, что Proxy :: Proxy '[Int, Float, Bool] аргумент construct, тем самым фиксируя выбор f. Это связано с тем, что вас не удерживают от типов f1 и f2 таких, что f1 ->> Val f1 ~ f2 ->> Val f2.

Не волнуйся, this shortcoming of the language is being looked at.