Translate a Scala Type example to Haskell

Question

I found a really interesting example in a Scala article and I am wondering how it might be encoded in Haskell.

trait Status
trait Open extends Status
trait Closed extends Status

trait Door[S <: Status]
object Door {
  def apply[S <: Status] = new Door[S] {}

  def open[S <: Closed](d: Door[S]) = Door[Open]
  def close[S <: Open](d: Door[S]) = Door[Closed]
}

val closedDoor = Door[Closed]
val openDoor = Door.open(closedDoor)
val closedAgainDoor = Door.close(openDoor)

//val closedClosedDoor = Door.close(closedDoor) // fails to compile
//val openOpenDoor = Door.open(openDoor) // fails to compile

This sample encodes at the type level that you can only open a closed Door, and only close an open Door. My first attempt was just using simple data types but doesn't work as intended:

data Status = Open | Closed deriving (Show)
data Door = Door Status deriving (Show)

open :: Door -> Door
open (Door Closed) = Door Open

close :: Door -> Door
close (Door Open) = Door Closed

main = do
  let closedDoor = (Door Closed)
  let openDoor = open closedDoor
  let closedAgainDoor = close openDoor
  let closeClosedDoor = close closedDoor
  let openOpenedDoor = open openDoor
  print closedAgainDoor

This actually compiles (unless I try to print closeClosedDoor or openOpenedDoor which then complains about non-exhaustive patterns in function open, which is obvious)

So I'm trying to figure out if GADTs our Type Families can accomplish this task, but I'm not able to grasp how yet.

Any ideas?

Answer 1

In addition to bheklilr's answer, you could use some type extensions to get even closer to the Scala example and rule out non-sensical types like

Door String

Using DataKinds, you could effectively disallow the phantom type from being anything but a Status.

{-# LANGUAGE DataKinds #-}

data Door (status :: Status) = Door
data Status = Open | Closed

open :: Door Closed -> Door Open
open _ = Door

close :: Door Open -> Door Closed
close _ = Door

Then, with type families, we could even define what it means to "toggle" a door

{-# LANGUAGE TypeFamilies #-}

type family Toggle (s :: Status) where
  Toggle Open = Closed
  Toggle Closed = Open

toggle :: Door s -> Door (Toggle s)
toggle Door = Door

---

As a closing thought, it may be nicer to use a GADT for Door - just so you have two different constructor names. I personally think this reads better

{-# LANGUAGE GADTs, DataKinds, TypeFamilies #-}

data Door (status :: Status) where
  OpenDoor :: Door Open
  ClosedDoor :: Door Closed

open :: Door Closed -> Door Open
open _ = OpenDoor

close :: Door Open -> Door Closed
close _ = ClosedDoor

toggle :: Door s -> Door (Toggle s)
toggle OpenDoor = ClosedDoor
toggle ClosedDoor = OpenDoor

Answer 2

I would do something like

data Open = Open deriving (Show)
data Closed = Closed deriving (Show)
data Door door_state = Door deriving (Show)

open :: Door Closed -> Door Open
open _ = Door

close :: Door Open -> Door Closed
close _ = Door

Now there aren't any cases to consider, the state itself is encoded in the type, as with the Scala example.