Does Haskell support closed polymorphic types?

Question

Given:

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

In the following code, I would like handle to be exactly one of three types: PlayerHandle, MinionHandle, and WeaponHandle. Is this possible to do in Haskell?

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

The following is too tedious:

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

EDIT:

Ørjan Johansen has proposed using closed type families, which indeed gets me a step closer to what I want. The issue I'm having using them is that I can't seem to write the following:

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

Here GHC complains that it cannot deduce that the handle is an instance of Show. I am hesitant to solve this by moving the Show constraint in the WithEach constructor for various reasons. These include modularity and scalability. Would something like a closed data family solve this (as I know type family mappings are not injective... Is that the problem even with closed ones?)

Answer 1

I think you can get precisely your syntax with a closed constraint type family:

{-# 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: Another attempt that includes 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

I don't quite see how to avoid having two different classes, types or families and get the API you seem to want without making it possible to add other types in another module. I also don't know of any way for the resulting IsHandle constraint to automatically inherit all the classes the three types have in common, without you listing them somewhere.

But I think depending on your needs/style, there are some more options similar to my last one:

• You could make IsHandle a class with IsHandle' and Show etc. as superclasses.
• You could make IsHandle' a class, in which case the only prevention against adding more types would be not exporting IsHandle'.

One advantage of the last one is that it can seriously cut down the number of extensions needed for this:

{-# LANGUAGE GADTs, ConstraintKinds #-}

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

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

Answer 2

Here's a solution based on 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

The idea here is to use a type witness HandleW a, certifying that a is one of your three types. Then, the "lemma" handlewShow proves that if HandleW a holds, then a must be a Show-able type.

It is also possible to generalize the code above to arbitrary type classes. The lemma below proves that if you have c T for each of your three types T, and you know that HandleW a holds, then c a must hold as well. You can obtain the previous lemma by picking 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 3

Add a type parameter to your Handle type, and restrict its values to be one of just three using DataKinds, thus:

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

Answer 4

Unless you want to do something complex with the type, I would go with a simple solution using 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 5

I'd use 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

Thanks for all the solutions guys. They all are helpful for various use cases. For my use case, it turned out that making the handle types into a single GADT solved my problem.

Here's my derived solution for those interested:

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