haskell - Haskell 有统一的吗？

Question

我正在研究单例类型可以在多大程度上模拟依赖类型并且我遇到了一个问题。我复制错误的最小代码是：

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeInType #-}

import Data.Kind(Type)

data SBool :: Bool -> Type where
  STrue :: SBool 'True
  SFalse :: SBool 'False

data SSBool :: SBool b -> Type where
  SSFalse :: SSBool 'SFalse
  SSTrue  :: SSBool 'STrue

错误信息是：

预期种类 'SBool b'，但 ''SFalse' 有种类 'SBool 'False'</p>

Answer 1

您需要明确依赖关系。以下使用 GHC 8.0.1 编译。

import Data.Kind(Type)

data SBool :: Bool -> Type where
  STrue :: SBool 'True
  SFalse :: SBool 'False

data SSBool :: forall (b :: Bool) . SBool b -> Type where
  SSFalse :: SSBool 'SFalse
  SSTrue  :: SSBool 'STrue

老实说，我对此感到惊讶。我根本不知道这种类型的依赖是被允许的。

请注意，这与 Coq 没有什么不同，其中

Inductive SSBool (b: bool) : SBool b -> Type :=
  | SSFalse : SSBool SFalse
  | SSTrue  : SSBool STrue
.

编译失败，而

Inductive SSBool : forall (b: bool), SBool b -> Type :=
  | SSFalse : SSBool false SFalse
  | SSTrue  : SSBool true STrue
.

编译。