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

错误信息是：

Expected kind ‘SBool b’, but ‘'SFalse’ has kind ‘SBool 'False’

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
.

编译。