如何创建一个返回两种不同类型的类型良好的函数？

Question

我对将Formality-Core模块编译为 Haskell 库非常感兴趣。虽然我可以unsafeCoerce在任何地方使用，但如果我能保留类型信息，允许编译模块在 Cabal 上发布并被其他 Haskell 项目使用，那就更有趣了。问题是依赖类型允许被 Haskell 禁止的程序。例如，foo下面的函数：

foo: (b : Bool) -> If(b)(Nat)(Bool)
  (b)
  b<(b) If(b)(Nat)(Bool)>
  | zero;
  | false;

根据输入返回不同的类型。如果输入为false，则返回数字zero。如果输入为true，则返回布尔值false。似乎这样的函数无法转换为 Haskell。我相信，在过去的几年里，Haskell 在依赖类型方面取得了很好的进展，所以，我想知道：有没有办法编写基于输入值返回不同类型的函数？

Answer 1

最先进的技术仍然是单例方法。

data SBool b where
  SFalse :: SBool 'False
  STrue :: SBool 'True

type family If (b :: Bool) (t1 :: k) (t2 :: k) :: k where
  If 'False x _ = x
  If 'True _ y = y

foo :: SBool b -> If b Natural Bool
foo SFalse = 0
foo STrue = False

Answer 2

GADTs + TypeFamilies（可选，+ DataKinds）可以大致做到这一点。所以：

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}

data GADTBool a where
    GADTFalse :: GADTBool False
    GADTTrue :: GADTBool True

type family If cond t f where
    If False t f = f
    If True  t f = t

foo :: GADTBool b -> If b Int Bool
foo GADTTrue = 0
foo GADTFalse = False

当然，foo :: GADTBool b -> If b (GADTInt 0) (GADTBool False)如果你打算普遍地做这种事情，你可能真的想要。您想要查看更多此类黑客示例的搜索词是“单例类型”，通常缩写为“单例”。