Подтвердить что ты не робот

Поддерживает ли Haskell закрытые полиморфные типы?

Дано:

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

В следующем коде я хотел бы, чтобы handle был точно одним из трех типов: PlayerHandle, MinionHandle и WeaponHandle. Возможно ли это сделать в 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

EDIT:

Ø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. Я не решаюсь это решить, перемещая ограничение Show в конструкторе WithEach по разным причинам. К ним относятся модульность и масштабируемость. Будет ли что-то вроде замкнутого семейства данных решить это (поскольку я знаю, что сопоставления семейства типов не являются инъективными... Это проблема даже с закрытыми?)

4b9b3361

ОТВЕТЫ

Ответ 1

Спасибо всем ребятам. Все они полезны для различных случаев использования. Для моего варианта использования оказалось, что превращение типов дескрипторов в один 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]

Ответ 2

Я думаю, вы можете получить именно ваш синтаксис с помощью семейства 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

EDIT: Еще одна попытка, включающая 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

Я не совсем понимаю, как избежать использования двух разных классов, типов или семейств и получить API, который вам кажется не нужен, без возможности добавления других типов в другой модуль. Я также не знаю, каким образом результирующее ограничение IsHandle автоматически наследует все классы, которые имеют три типа, без каких-либо ссылок на них.

Но я думаю, что в зависимости от ваших потребностей/стиля есть еще несколько вариантов, похожих на мой последний:

  • Вы можете сделать IsHandle класс с IsHandle' и Show и т.д. в качестве суперклассов.
  • Вы можете сделать IsHandle' класс, и в этом случае единственная защита от добавления большего количества типов не будет экспортировать IsHandle'.

Одним из преимуществ последнего является то, что он может серьезно сократить количество необходимых для этого расширений:

{-# LANGUAGE GADTs, ConstraintKinds #-}

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

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

Ответ 3

Здесь решение, основанное на 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 является одним из трех ваших типов. Тогда "лемма" handlewShow доказывает, что если HandleW a выполняется, то a должен быть Show -устойчивым типом.

Также можно обобщить приведенный выше код на произвольные классы типов. Лемма ниже доказывает, что если у вас есть c T для каждого из трёх типов 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

Ответ 4

Добавьте параметр типа к типу 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

Ответ 5

Если вы не хотите делать что-то сложное с типом, я бы пошел с простым решением, используя 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

Ответ 6

Я бы использовал 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