haskell - 单例的单例(在 Haskell 中模拟复杂的 pi 类型)

Question

我在 Idris 中有一个简单的概念证明，它使用依赖类型来执行一些不太复杂的业务逻辑。一些名称已更改以保护不那么无辜的人，但我们的想法是我们希望按顺序收集“行”。每一行都属于一个特定的部分，但只有一个 (EconProduction) 包含我们关心的任何内容。通常，行有一个特定于节的关键字和一个表达式，其形式/类型可能取决于所使用的关键字。

对于这个特定的部分，每一行要么描述“阶段”的一些数字(Prod)，要么继续最后命名的“阶段”(Continue)。

在 Idris 中，我们可以这样做:

data EconSection
  = EconGeneral
  | EconProduction

data EconPhase
  = Oil
  | Water
  | NumPhase Nat

data ContState
  = ContNone
  | ContProd EconPhase

data Keyword : EconSection -> ContState -> ContState -> Type where
  Prod : (p : EconPhase) -> Keyword EconProduction c (ContProd p)
  Continue : Keyword s c c

data Expression : (s : EconSection) ->
                  (d : ContState) ->
                  Keyword s c d ->
                  Type where
  ExProc : Double -> Double -> Expression EconProduction (ContProd p) k

data Line : EconSection -> ContState -> ContState -> Type where
  L : (k : Keyword s c d) -> Expression s d k -> Line s c d

data Lines : EconSection -> ContState -> Type where
  First : Line s ContNone d -> Lines s d
  Then : Lines s c -> Line s c d -> Lines s d

infixl 0 `Then`

good : Lines EconProduction (ContProd (NumPhase 1))
good = First (L (Prod Oil) (ExProc 23.2 70.1))
      `Then` (L (Continue) (ExProc 27.9 1.2))
      `Then` (L (Prod (NumPhase 1)) (ExProc 91.2 7014.1))
      `Then` (L (Continue) (ExProc 91.2 7014.1))

到目前为止，一切都很好!通常的依赖类型状态业务。出于非常实际的商业原因，我们希望在 GHC Haskell 中实际实现这个逻辑。我用单例构建了它(根据需要滚动我自己的而不是使用 singletons 包，只是为了简短的概念证明):

{-# LANGUAGE GADTs, KindSignatures, DataKinds #-}
{-# LANGUAGE RankNTypes, TypeInType, TypeOperators #-}
{-# LANGUAGE TypeFamilies, TypeFamilyDependencies, MultiParamTypeClasses #-}

import Data.Kind (Type)

data Nat
  = Z
  | S Nat

data SNat :: Nat -> Type where
  SZ :: SNat 'Z
  SS :: SNat n -> SNat ('S n)

data SSNat :: forall (n :: Nat) . SNat n -> Type where
  SSZ :: SSNat 'SZ
  SSS :: SSNat n -> SSNat ('SS n)

type family SingNat (n :: Nat) :: SNat n where
  SingNat 'Z = 'SZ
  SingNat ('S n) = 'SS (SingNat n)

data EconSection
  = EconGeneral
  | EconProduction

data SEconSection :: EconSection -> Type where
  SEconGeneral :: SEconSection 'EconGeneral
  SEconProduction :: SEconSection 'EconProduction

type family SingSection (s :: EconSection) :: SEconSection s where
  SingSection 'EconGeneral = 'SEconGeneral
  SingSection 'EconProduction = 'SEconProduction 

data EconPhase
  = Oil
  | Water
  | NumPhase Nat

data SEconPhase :: EconPhase -> Type where
  SOil :: SEconPhase 'Oil
  SWater :: SEconPhase 'Water
  SNumPhase :: SNat n -> SEconPhase ('NumPhase n)

data SSEconPhase :: forall (p :: EconPhase) . SEconPhase p -> Type where
  SSOil :: SSEconPhase 'SOil
  SSWater :: SSEconPhase 'SWater
  SSNumPhase :: SSNat n -> SSEconPhase ('SNumPhase n)

type family SingEconPhase (p :: EconPhase) :: SEconPhase p where
  SingEconPhase 'Oil = 'SOil
  SingEconPhase 'Water = 'SWater
  SingEconPhase ('NumPhase n) = 'SNumPhase (SingNat n)

data ContState
  = ContNone
  | ContProd EconPhase

data SContState :: ContState -> Type where
  SContNone :: SContState 'ContNone
  SContProd :: SEconPhase p -> SContState ('ContProd p)

type family SingContState (c :: ContState) :: SContState c where
  SingContState 'ContNone = 'SContNone
  SingContState (ContProd p) = 'SContProd (SingEconPhase p)

data Keyword :: EconSection -> ContState -> ContState -> Type where
  Prod :: SEconPhase p -> Keyword 'EconProduction c ('ContProd p)
  Continue :: Keyword s c c

data SKeyword :: forall (s :: EconSection) (c :: ContState) (d :: ContState) .
                 Keyword s c d -> Type where
  SProd :: SSEconPhase p -> SKeyword ('Prod p)
  SContinue :: SKeyword 'Continue

data Expression :: forall (s :: EconSection) (c :: ContState) (d :: ContState) .
                   SEconSection s -> SContState d -> Keyword s c d -> Type where
  ExProc :: Double -> Double -> Expression SEconProduction (SContProd p) k

type family KWSection k where
  KWSection (Keyword s _ _) = s

type family KWFrom k where
  KWFrom (Keyword _ c _) = c

type family KWTo k where
  KWTo (Keyword _ _ d) = d

data Line :: EconSection -> ContState -> ContState -> Type where
  L :: SKeyword (k :: Keyword s c d)
    -> Expression (SingSection s) (SingContState d) k
    -> Line s c d

data Lines :: EconSection -> ContState -> Type where
  First :: Line s 'ContNone d -> Lines s d
  Then :: Lines s c -> Line s c d -> Lines s d

infixl 0 `Then`

good :: Lines 'EconProduction ('ContProd ('NumPhase ('S 'Z)))
good = First (L (SProd SSOil) (ExProc 23.2 70.1))
      `Then` (L (SContinue) (ExProc 27.9 1.2))
      `Then` (L (SProd (SSNumPhase (SSS SSZ))) (ExProc 91.2 7014.1))
      `Then` (L (SContinue) (ExProc 91.2 7014.1))

这是我的问题。有什么办法可以避免“单例中的单例”？我不喜欢 SSNat 之类的东西的外观等等，但这是我通过将每个 pi 类型转换为额外的单例层而得到的。我无法使任何更简单的方法发挥作用，而且我在 singletons 中也没有看到任何聪明的想法。包以使这更容易，尽管我可能很容易错过所有模板 Haskell 下的某些内容。

Answer 1

是的。

考虑一下，根据单例类型的定义，单例中的类型信息与该单例的单例一样多，因为它们都有唯一的实例。

在您的代码中

考虑到上述情况，我们可以删除 SSNat和 SSEconPhase您的代码中的声明。然后，在 SProd构造函数

SProd :: SSEconPhase p - > SKeyword ('Prod p)

我们知道 SEconPhase足以决定 p ，所以我们可以将其重写为

SProd :: SEconPhase p - > SKeyword ('Prod p)

这会产生一个错误——我们需要的是一个类型转换，比如

SomeType :: (p :: EconPhase) -> SEconPhase p

您已经在代码中定义为 SingEconPhase .结果是

SProd :: SEconPhase p - > SKeyword ('Prod (SingEconPhase p))

一般来说

您永远不必编写单例的单例 - 如果您需要将类型参数“提升”到单例类型，那么正确的选择是像您所做的那样编写类型族。