Czy Haskell obsługuje zamknięte typy polimorficzne?

Question

Dane:

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

W poniższym kodzie, chciałbym handle być dokładnie jeden z trzech rodzajów: PlayerHandle, MinionHandle i WeaponHandle. Czy można to zrobić w Haskell?

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

Poniżej zbyt uciążliwe:

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

EDIT:

Ørjan Johansen zaproponował przy użyciu zamkniętych typu rodzin, które rzeczywiście robi mi to krok bliżej do tego, co chcę. Problem mam korzystania z nich jest to, że nie może wydawać się, aby napisać następujące:

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 

Tutaj GHC narzeka, że ​​nie można wywnioskować, że uchwyt jest instancją Show. Jestem niezdecydowany, aby rozwiązać ten problem, przenosząc ograniczenie Show do konstruktora WithEach z różnych powodów. Należą do nich modułowość i skalowalność. Czy rozwiązałoby to coś takiego, jak rodzina danych zamkniętych (jak wiem, rodzinne mapowania nie są iniekcyjne ... Czy to jest problem nawet w przypadku zamkniętych?)

Answer 1

Dzięki za wszystkie rozwiązania facetów. Wszystkie są pomocne w różnych przypadkach użycia. Dla mojego przypadku użycia okazało się, że przekształcenie typów uchwytów w jeden GADT rozwiązało mój problem.

Oto moje rozwiązanie pochodzące dla zainteresowanych:

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

Answer 2

Myślę, że możesz dokładnie uzyskać swoją składnię z rodziną typu closedconstraint :

{-# 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: Kolejna próba, która obejmuje 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 

ja nie bardzo rozumiem, jak uniknąć dwóch różnych klas, typów lub rodzin i uzyskać API to wydaje się w mrówka bez możliwości dodawania innych typów w innym module. Nie wiem też w żaden sposób, aby wynikające z tego więzienie IsHandle automatycznie dziedziczyło wszystkie klasy wspólne dla tych trzech typów, bez wymieniania ich gdzieś gdzieś na.

Ale myślę, że w zależności od potrzeb/stylu, istnieje kilka opcji podobnie jak moja ostatnia:

• Można zrobić IsHandle klasę z IsHandle' i Show itp jako nadrzędnych.
• Można uczynić klasę IsHandle', w którym to przypadku jedynym sposobem zapobiegania dodawaniu kolejnych typów nie byłoby eksportowanie IsHandle'.

Zaletą tej ostatniej jest, że może poważnie obniżyć liczbę rozszerzeń potrzebnych do tego:

{-# LANGUAGE GADTs, ConstraintKinds #-} 

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

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

Answer 3

Chyba że chcesz zrobić kompleks coś z typem, pójdę z proste rozwiązanie za pomocą 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 

Answer 4

Oto rozwiązanie oparte na GADTs:

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

Chodzi o to, aby użyć świadka typu HandleW a, potwierdzając, że a jest jednym z trzech typów. Następnie "lemma" handlewShow udowadnia, że ​​jeśli HandleW a zachowuje, to a musi być typu nadającego się do użytku .

Możliwe jest również uogólnienie powyższego kodu na dowolne klasy typów. Poniższy lemat udowodni, że jeśli masz c T dla każdego z trzech typów T i wiesz, że HandleW a ma, to musi również zawierać. Możesz uzyskać poprzedni lemat, wybierając 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 

Answer 5

użyję GADTs:

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

Answer 6

Dodaj parametr typu do typu Handle i ograniczyć jej wartości będzie jedną z zaledwie trzech użyciu DataKinds, a więc:

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