相当于 Kotlin 不变类型的 Haskell

Question

在科特林我可以做

sealed class Substance {
    object Uranus : Substance()
    object Mercury: Substance()
    object Ammonia : Substance()
}

data class DangerousBox<T : Substance>(val item: T)

fun main() {
    val uranus = DangerousBox<Substance.Uranus>(Substance.Uranus)
    val mercury: DangerousBox<Substance.Mercury> = uranus
}

现在我有不变的类型DangerousBox<Substance.Uranus>, DangerousBox<Substance.Mercury>等，所以上面的示例将无法编译。

如何在 Haskell 中做到这一点？

理想情况下我想要类型

uranus :: DangerousBox Uranus
uranus = DangerousBox Mercury

这个样本也不能符合。

我尝试通过以下方式来实现：

1. 模块化约束。我有模块

module Sample.Types.Boxes
  ( Substance(..)
  , dangerousBox
  , VDangerousBox {- no Con-}
  ) where

data Substance
  = Uranus
  | Mercury
  | Ammonia
  deriving (Show)

data VDangerousBox a =
  VDangerousBox Substance
  deriving (Show)

dangerousBox :: Substance -> VDangerousBox Substance
dangerousBox a = VDangerousBox a

模块的客户端只能使用危险框，但这里我有与物质相关的 jeneric：

uranus :: VDangerousBox Substance
uranus = dangerousBox Uranus

2. 数据种类

data DangerousBox :: Substance -> * where
  DangerousBox :: Substance -> DangerousBox a

uranus :: DangerousBox Uranus
uranus = DangerousBox Uranus

mercury :: DangerousBox Mercury
mercury = uranus {- it's ok, it dosn't compile -}

但在这种情况下，以下情况将编译：

mercury :: DangerousBox Mercury
mercury = DangerousBox Ammonia

我了解我已收到同等金额

data Box<T : Substance>(val value: Substance)

就 Kotlin 泛型而言。

这不是真实的案例，只是出于“学术”兴趣。

Answer 1

因为，给定特定的物质选择，框中没有任何其他信息包含（至少在您的 Kotlin 代码中），所以我首先考虑完全忽略它：

import Data.Kind (Type)  -- preferred version instead of the old *

data DangerousBox :: Substance -> Type where
  DangerousBox :: DangerousBox a

uranus :: DangerousBox Uranus
uranus = DangerousBox

那么mercury = DangerousBox Ammonia问题就不会出现，因为DangerousBox值构造函数不接受任何参数。

如果由于某种原因您确实需要一个代表标记类型的实际值，那么这不应该是标记本身作为值Type，因为在该视图中Uranus、Mercury和Ammonia都是相同的类型。相反，您应该使用通常所说的这些类型的单例。您可以自动生成它们，或手动定义它们：

data SubstanceSing :: Substance -> Type where
  UranusS :: SubstanceSing 'Uranus
  MercuryS :: SubstanceSing 'Mercury
  AmmoniaS :: SubstanceSing 'Ammonia

现在出现在值级别时UranusS对应于您的 Kotlin 。Substance.Uranus然后你的盒子类型就变成了

data DangerousBox :: Substance -> Type where
  DangerousBox :: SubstanceSing a -> DangerousBox a