将 Scala 类型示例转换为 Haskell答案

【问题标题】：Translate a Scala Type example to Haskell将 Scala 类型示例转换为 Haskell
【发布时间】：2017-04-17 19:04:59
【问题描述】：

我在一篇 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，然后抱怨打开函数中的非详尽模式，这很明显）

所以我想弄清楚我们的类型家族的 GADT 是否可以完成这项任务，但我还不知道怎么做。

有什么想法吗？

【问题讨论】：

标签： scala haskell types functional-programming

【解决方案1】：

除了 bheklilr 的回答之外，您还可以使用一些类型扩展来更接近 Scala 示例并排除无意义的类型，例如

Door String

使用DataKinds，您可以有效地禁止幻像类型不是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

作为结束的想法，为Door 使用 GADT 可能会更好——这样你就有两个不同的构造函数名称。我个人认为这读起来更好

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

【讨论】：

你打败了我DataKinds 答案。我不想在没有先检查编译的情况下发布它，但我必须先运行stack setup，这在慢速网络上需要一段时间，哈哈。我喜欢 toggle 和 TypeFamilies 的想法，但没想到。
很好，我想我自己不会来这个，还在学习该语言的高级功能。
为了更好的推理，toggle :: (s ~ Toggle t, t ~ Toggle s) => Door s -> Door t。或class Toggled s t | s -> t, t -> s where toggle :: Door s -> Door t。您可能会为 GHC 8 使用单射类型系列，但我还没有购买。
@dfeuer 巧妙的推理技巧！是什么让您想到它（即，这是更一般模式的特例）？
@Alec，这当然是更一般模式的特例！当你的类型族是单射的时，你应该总是考虑它。但即使不是，也要寻找机会根据一个或多个其他类型变量来约束每个类型变量。

【解决方案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 示例一样。

【讨论】：