haskell - 封闭类型族中的种类多态性

Question

我试图Ty从计算. Atom我首先尝试使用一个封闭的类型族，就像论文所做的那样：

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

module GenericK where

import Data.Kind

type Kind = Type

-- | TyVar represents type parameters that the data takes
data TyVar (zeta :: Kind) (k :: Kind) :: Type where
  VZ :: TyVar (x -> xs) x
  VS :: TyVar xs k -> TyVar (x -> xs) k

-- | Atom is similar to K1
data Atom (zeta :: Kind) (k :: Kind) :: Type where
  Var :: TyVar zeta k -> Atom zeta k
  Kon :: k -> Atom zeta k
  (:@:) :: Atom zeta (l -> k) -> Atom zeta l -> Atom zeta k

--| Gamma is a context
data Gamma (zeta :: Kind) where
  Eta :: Gamma Type
  (:&:) :: k -> Gamma ks -> Gamma (k -> ks)

type family Ty zeta (alpha :: Gamma zeta) (t :: Atom zeta k) :: k where
  Ty (k -> ks) (t :&: alpha) (Var VZ) = t
  Ty (k -> ks) (t :&: alpha) (Var (VS v)) = Ty ks alpha (Var v)
  Ty zeta alpha (Kon t) = t
  Ty zeta alpha (f :@: x) = (Ty zeta alpha f) (Ty zeta alpha x)

然而，GHC 抱怨道：

• Expected kind ‘Atom zeta k’,
    but ‘f’ has kind ‘Atom zeta (k -> k)’
• In the third argument of ‘Ty’, namely ‘f’
  In the type ‘(Ty zeta alpha f) (Ty zeta alpha x)’
  In the type family declaration for ‘Ty’

该错误消息对我来说没有多大意义，因为显然f应该有 kindAtom zeta (l -> k)并且x应该有 kind Atom zeta l。

所以我尝试使用一个开放类型的系列并且它起作用了：

type family Ty zeta (alpha :: Gamma zeta) (t :: Atom zeta k) :: k

type instance Ty (k -> ks) (t :&: alpha) (Var VZ) = t
type instance Ty (k -> ks) (t :&: alpha) (Var (VS v)) = Ty ks alpha (Var v)
type instance Ty zeta alpha (Kon t) = t
type instance Ty zeta alpha (f :@: x) = (Ty zeta alpha f) (Ty zeta alpha x)

我很好奇为什么封闭式家庭不起作用。我想这可能与种类多态性有关，但我真的不知道种类检查在 GHC 中是如何工作的。

标签： haskellgeneric-programmingtype-families