Sing.hs

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

import Data.Function ((&))
import Control.Monad (foldM)
import Text.Read (readMaybe)

data DoorState = Opened | Closed
  deriving Show

data SDoorState (s :: DoorState) where
  SClosed :: SDoorState Closed
  SOpened :: SDoorState Opened

deriving instance Show (SDoorState s)

class SDoorStateI (s :: DoorState) where
  sState :: SDoorState s

instance SDoorStateI Opened where
  sState = SOpened

instance SDoorStateI Closed where
  sState = SClosed

data Door (s :: DoorState) where
  MkDoor :: Door Closed
  Open :: Door Closed -> Door Opened
  Close :: Door Opened -> Door Closed
  Hold :: Door s -> Door s

deriving instance Show (Door s)

openedDoor = Open MkDoor

-- badDoor = Close MkDoor

someDoor = MkDoor & Open & Hold & Hold & Close & Hold & Open 
-- (&) = flip ($) -- imported from Data.Function (base)

data AnyDoor where
  AnyDoor :: SDoorStateI s => Door s -> AnyDoor

deriving instance Show AnyDoor

sDoorState :: SDoorStateI s => Door s -> SDoorState s
sDoorState _ = sState

applyCmd :: AnyDoor -> String -> Maybe AnyDoor
applyCmd (AnyDoor d) cmd =
  case (sDoorState d, cmd) of
    (SClosed, "Open") -> Just $ AnyDoor $ Open d
    (SOpened, "Close") -> Just $ AnyDoor $ Close d
    (_, "Hold") -> Just $ AnyDoor $ Hold d
    _ -> Nothing

parseDoor :: String -> Maybe AnyDoor
parseDoor =
  foldM applyCmd (AnyDoor MkDoor) . words

testDoor :: Maybe AnyDoor
testDoor = parseDoor "Open Hold Hold Close Hold Open Hold Close Open"

-- Exercise

extractDoor :: AnyDoor ->
               Either (Door Closed) (Door Opened)
extractDoor = undefined

-- The best tutorial on the singletons library:
-- https://blog.jle.im/entries/series/+introduction-to-singletons.html

main = print testDoor