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