haskell - 将类型级列表 '[a,b,c,...] 转换为函数 a->b->c->

Question

我有一个由类型级别列表索引的数据系列，其中列表中的类型对应于数据实例的参数。
我想根据数据实例编写具有不同数量和参数的函数，所以我可以像使用同义词一样使用它作为家族中每个数据实例的同义词。

{-# 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

您的代码无法进行类型检查，因为 type families are not (necessarily) injective .如果您通过指定 f 的选择来帮助 GHC在 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 .