Перевести пример Scala типа Haskell

Я нашел действительно интересный пример в статье Scala, и мне интересно, как это можно закодировать в 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

Этот образец кодируется на уровне типа, который можно открыть только закрытым Door, и закрыть только Door. Моя первая попытка заключалась в простом использовании простых типов данных, но не работает должным образом:

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

Это фактически компилируется (если я не пытаюсь напечатать closeClosedDoor или openOpenedDoor, который затем жалуется на неисчерпывающие шаблоны в функции open, что очевидно)

Итак, я пытаюсь выяснить, могут ли GADTs наши семейства типов выполнить эту задачу, но пока я не могу понять.

Любые идеи?

Ответ 1

В дополнение к ответу bheklilr вы можете использовать некоторые расширения типов, чтобы приблизиться к примеру Scala и исключить нечувствительные типы, такие как

Door String

Используя DataKinds, вы можете эффективно запретить тип phantom быть чем угодно, кроме 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

Затем, с семействами типов, мы могли бы даже определить, что значит "переключать" дверь

{-# LANGUAGE TypeFamilies #-}

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

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

Как заключительная мысль, может быть лучше использовать GADT для Door - так, чтобы у вас было два разных имени конструктора. Я лично считаю, что это лучше читается

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

Ответ 2

Я бы сделал что-то вроде

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

Теперь нет никаких случаев для рассмотрения, само состояние кодируется в типе, как в примере Scala.