Haskell 是否支持封闭多态类型?

Does Haskell support closed polymorphic types?

给定:

newtype PlayerHandle = PlayerHandle Int deriving (Show)
newtype MinionHandle = MinionHandle Int deriving (Show)
newtype WeaponHandle = WeaponHandle Int deriving (Show)

在下面的代码中,我希望 handle 恰好 三种类型之一:PlayerHandleMinionHandleWeaponHandle。这可以在 Haskell 中完成吗?

data Effect where
    WithEach :: (??? handle) => [handle] -> (handle -> Effect) -> Effect -- Want `handle' to be under closed set of types.

下面太冗长了:

data Effect' where
    WithEachPlayer :: [PlayerHandle] -> (PlayerHandle -> Effect) -> Effect
    WithEachMinion :: [MinionHandle] -> (MinionHandle -> Effect) -> Effect
    WithEachWeapon :: [WeaponHandle] -> (WeaponHandle -> Effect) -> Effect

编辑:

Ørjan Johansen 提议使用封闭类型族,这确实让我离我想要的更近了一步。我在使用它们时遇到的问题是我似乎无法编写以下内容:

type family IsHandle h :: Constraint where
    IsHandle (PlayerHandle) = ()
    IsHandle (MinionHandle) = ()
    IsHandle (WeaponHandle) = ()

data Effect where
    WithEach :: (IsHandle handle) => [handle] -> (handle -> Effect) -> Effect

enactEffect :: Effect -> IO ()
enactEffect (WithEach handles cont) = forM_ handles $ \handle -> do
    print handle  -- Eeek! Can't deduce Show, despite all cases being instances of Show.
    enactEffect $ cont handle

这里 GHC 抱怨它不能推断句柄是 Show 的一个实例。出于各种原因,我对通过在 WithEach 构造函数中移动 Show 约束来解决这个问题犹豫不决。这些包括模块化和可扩展性。像封闭数据族这样的东西会解决这个问题吗(据我所知,类型族映射不是单射的......即使是封闭的也是这个问题吗?)

我认为您可以使用 closed constraint 类型族准确地获得语法:

{-# LANGUAGE TypeFamilies, ConstraintKinds, GADTs #-}

import GHC.Exts (Constraint)

newtype PlayerHandle = PlayerHandle Int
newtype MinionHandle = MinionHandle Int
newtype WeaponHandle = WeaponHandle Int

type family IsHandle h :: Constraint where
    IsHandle (PlayerHandle) = ()
    IsHandle (MinionHandle) = ()
    IsHandle (WeaponHandle) = ()

data Effect where
    WithEach :: (IsHandle handle) => [handle] -> (handle -> Effect) -> Effect

编辑:另一种尝试,包括 Show:

{-# LANGUAGE TypeFamilies, ConstraintKinds, GADTs,
             UndecidableInstances #-}

import GHC.Exts (Constraint)
import Control.Monad (forM_)

newtype PlayerHandle = PlayerHandle Int
newtype MinionHandle = MinionHandle Int
newtype WeaponHandle = WeaponHandle Int

type family IsHandle' h :: Constraint where
    IsHandle' (PlayerHandle) = ()
    IsHandle' (MinionHandle) = ()
    IsHandle' (WeaponHandle) = ()

type IsHandle h = (IsHandle' h, Show h)

data Effect where
    WithEach :: (IsHandle handle) => [handle] -> (handle -> Effect) -> Effect

-- Assume my each (IsHandle a) already is an instance of a class I want to use, such as (Show).
enactEffect :: Effect -> IO ()
enactEffect (WithEach handles cont) = forM_ handles $ \handle -> do
    print handle  -- (*)
    enactEffect $ cont handle

我不太明白如何避免拥有两个不同的 classes、类型或系列并获得您似乎想要的 API 而无需在另一个模块中添加其他类型.我也不知道有什么方法可以使生成的 IsHandle 约束自动继承这三种类型共有的所有 classes,而无需在 某处列出它们 .

但我认为根据您的 needs/style,还有一些与我的上一个类似的选项:

  • 你可以用 IsHandle'Show 等使 IsHandle 成为 class 作为 superclasses.
  • 您可以将 IsHandle' 设为 class,在这种情况下,防止添加更多类型的唯一方法就是不导出 IsHandle'

最后一个的一个优点是它可以大大减少为此所需的扩展数量:

{-# LANGUAGE GADTs, ConstraintKinds #-}

class IsHandle' h
instance IsHandle' (PlayerHandle)
instance IsHandle' (MinionHandle)
instance IsHandle' (WeaponHandle)

type IsHandle h = (IsHandle' h, Show h)

除非你想对类型做一些复杂的事情,否则我会使用一个简单的解决方案 class:

{-# LANGUAGE GADTs #-}

import Control.Monad

newtype PlayerHandle = PlayerHandle Int deriving (Show)
newtype MinionHandle = MinionHandle Int deriving (Show)
newtype WeaponHandle = WeaponHandle Int deriving (Show)

class (Show h) => Handle h
instance Handle PlayerHandle
instance Handle MinionHandle
instance Handle WeaponHandle

data Effect where
    WithEach :: (Handle handle) => [handle] -> (handle -> Effect) -> Effect

enactEffect :: Effect -> IO ()
enactEffect (WithEach handles cont) = forM_ handles $ \handle -> do
    print handle
    enactEffect $ cont handle

这是一个基于 GADT 的解决方案:

{-# LANGUAGE GADTs, RankNTypes #-}
{-# OPTIONS -Wall #-}
module GADThandle where

import Control.Monad

newtype PlayerHandle = PlayerHandle Int deriving (Show)
newtype MinionHandle = MinionHandle Int deriving (Show)
newtype WeaponHandle = WeaponHandle Int deriving (Show)

data HandleW a where
   WPlayer :: HandleW PlayerHandle
   WMinion :: HandleW MinionHandle
   WWeapon :: HandleW WeaponHandle

handlewShow :: HandleW a -> (Show a => b) -> b
handlewShow WPlayer x = x
handlewShow WMinion x = x
handlewShow WWeapon x = x

data Effect where
   WithEach :: HandleW handle -> [handle] -> (handle -> Effect) -> Effect 

enactEffect :: Effect -> IO ()
enactEffect (WithEach handlew handles cont) = handlewShow handlew $ 
   forM_ handles $ \handle -> do
      print handle
      enactEffect $ cont handle

这里的想法是使用类型见证 HandleW a,证明 a 是您的三种类型之一。然后,"lemma" handlewShow证明如果HandleW a成立,那么a一定是Show-able类型。

也可以将上面的代码泛化为任意类型 类。下面的引理证明,如果你的三种类型 T 中的每一种都有 c T,并且你知道 HandleW a 成立,那么 c a 也必须成立。您可以通过选择 c = Show.

来获得前面的引理
handlewC :: (c PlayerHandle, c MinionHandle, c WeaponHandle) => 
   HandleW a -> Proxy c -> (c a => b) -> b
handlewC WPlayer Proxy x = x
handlewC WMinion Proxy x = x
handlewC WWeapon Proxy x = x

enactEffect' :: Effect -> IO ()
enactEffect' (WithEach handlew handles cont) = handlewC handlew (Proxy :: Proxy Show) $ 
   forM_ handles $ \handle -> do
      print handle
      enactEffect' $ cont handle

我会使用 GADT:

{-# LANGUAGE KindSignatures, GADTs, RankNTypes, DataKinds #-}

data K = Player | Minion | Weapon
  deriving (Eq, Show)

newtype PlayerHandle = PlayerHandle Int deriving (Show)
newtype MinionHandle = MinionHandle Int deriving (Show)
newtype WeaponHandle = WeaponHandle Int deriving (Show)

-- Plain ADT might be enough
-- see below
data Handle (k :: K) where
  PlayerHandle' :: PlayerHandle -> Handle Player
  MinionHandle' :: MinionHandle -> Handle Minion
  WeaponHandle' :: WeaponHandle -> Handle Weapon

data SomeHandle where
  SomeHandle :: Handle k -> SomeHandle

data Effect where
  WithEach :: (SomeHandle -> IO ()) -> Effect

printEffect :: Effect
printEffect = WithEach f
  where f (SomeHandle h) = g h
        g :: Handle k -> IO ()
        g (PlayerHandle' p) = putStrLn $ "player :" ++ show p
        g (MinionHandle' p) = putStrLn $ "minion :" ++ show p
        g (WeaponHandle' p) = putStrLn $ "weapon :" ++ show p

-- GADTs are useful, if you want to have maps preserving handle kind:
data HandleMap where
  -- HandleMap have to handle all `k`, yet cannot change it!
  HandleMap :: (forall k. Handle k -> Handle k) -> HandleMap

zeroWeaponHandle :: HandleMap
zeroWeaponHandle = HandleMap f
  where f :: forall k. Handle k -> Handle k
        f (PlayerHandle' h) = PlayerHandle' h
        f (MinionHandle' h) = MinionHandle' h
        f (WeaponHandle' _) = WeaponHandle' $ WeaponHandle 0

向您的 Handle 类型添加一个类型参数,并使用 DataKinds 将其值限制为三个之一,因此:

{-# LANGUAGE DataKinds      #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs          #-}

import Control.Monad

data Entity = Player | Minion | Weapon

newtype Handle (e :: Entity) = Handle Int
    deriving (Eq, Ord, Read, Show)

data Effect where
    WithEach :: [Handle e] -> (Handle e -> Effect) -> Effect

enactEffect :: Effect -> IO ()
enactEffect (WithEach handles cont) = forM_ handles $ \handle -> do
    print handle
    enactEffect $ cont handle

感谢所有提供解决方案的人。它们都有助于各种用例。对于我的用例,事实证明将句柄类型变成单个 GADT 解决了我的问题。

这是我为那些感兴趣的人派生的解决方案:

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}

data Player
data Minion
data Weapon

data Handle a where
    PlayerHandle :: Int -> Handle Player
    MinionHandle :: Int -> Handle Minion
    WeaponHandle :: Int -> Handle Weapon

data Effect where
    WithEach :: [Handle h] -> (Handle h -> Effect) -> Effect
    PrintSecret :: Handle h -> Effect

-------------------------------------------------------------------------------
-- Pretend the below code is a separate file that imports the above data types
-------------------------------------------------------------------------------

class ObtainSecret a where
    obtainSecret :: a -> String

instance ObtainSecret (Handle a) where
    obtainSecret = \case
        PlayerHandle n -> "Player" ++ show n
        MinionHandle n -> "Minion" ++ show n
        WeaponHandle n -> "Weapon" ++ show n

enactEffect :: Effect -> IO ()
enactEffect = \case
    WithEach handles continuation -> mapM_ (enactEffect . continuation) handles
    PrintSecret handle -> putStrLn (obtainSecret handle)

createEffect :: [Handle h] -> Effect
createEffect handles = WithEach handles PrintSecret

main :: IO ()
main = do
    enactEffect $ createEffect $ map PlayerHandle [0..2]
    enactEffect $ createEffect $ map MinionHandle [3..5]
    enactEffect $ createEffect $ map WeaponHandle [6..9]