将存在性提升到类型级别

Question

tl; dr：我正在尝试重写一些具有Haskell中sigma类型列表的依存类型代码，而我似乎无法为存在性生成单例，换句话说，此代码失败了：

data Foo :: Type where
  Foo :: forall foo. Sing foo -> Foo

$(genSingletons [''Foo])

---

之后是更长的版本。

假定此Idris代码为模型：

data AddrType = Post | Email | Office

data AddrFields : AddrType -> Type where
  PostFields : (city : String) -> (street : String) -> AddrFields Post
  EmailFields : (email : String) -> AddrFields Email
  OfficeFields : (floor : Int) -> (desk : Nat) -> AddrFields Office

Addr : Type
Addr = (t : AddrType ** AddrFields t)

someCoolPredicate : List AddrType -> Bool

data AddrList : List Addr -> Type where
  MkAddrList : (lst : List Addr) -> {auto prf : So (someCoolPredicate lst)} -> AddrList lst

[基本上，当我们得到类型为AddrList lst的值时，我们知道lst : List Addr，并且someCoolPredicate适用于该列表。

我在现代Haskell中设法实现的最接近的假设是singletons-2.5：

import Data.Singletons.TH
import Data.Singletons.Prelude
import Data.Singletons.Prelude.List

data AddrType = Post | Email | Office
              deriving (Eq, Ord, Show)

$(genSingletons [''AddrType])
$(singEqInstances [''AddrType])

data family AddrFields (a :: AddrType)

data instance AddrFields 'Post    = PostFields { city :: String, street :: String } deriving (Eq, Ord, Show)
data instance AddrFields 'Email   = EmailFields { email :: String } deriving (Eq, Ord, Show)
data instance AddrFields 'Office  = OfficeFields { flr :: Int, desk :: Int} deriving (Eq, Ord, Show)

data Addr :: Type where
  Addr :: { addrType :: Sing addrType
          , addrTypeVal :: AddrType
          , fields :: AddrFields addrType
          } -> Addr

$(promote [d|
  someCoolPredicate :: [Addr] -> Bool
  someCoolPredicate = ...
  |])

data AddrList :: [Addr] -> Type where
  AddrList :: { addrs :: Sing addrs, prf :: SomeCoolPredicate addrs :~: 'True } -> AddrList addrs

但是在给定[Addr]的情况下，我实际上如何构造这种类型的值？换句话说，我该如何在Idris中表达以下内容？

*Addrs> MkAddrList [(Post ** PostFields "Foo" "Bar")]
MkAddrList [(Post ** PostFields "Foo" "Bar")] : AddrList [(Post ** PostFields "Foo" "Bar")]

问题是，看起来我必须能够执行toSing列表中的Addr或等效功能，但是$(genSingletons [''Addr])失败。确实，即使tl; dr部分中的代码也会失败。那么，除了放弃这个想法，我该怎么办？

Answer 1

此问题的解决方案需要单例的单例，这些单例在singletons-2.6中引入。首先，所需的语言扩展和导入：

{-# LANGUAGE TemplateHaskell, GADTs, ScopedTypeVariables, PolyKinds, DataKinds,
             TypeFamilies, TypeOperators, UndecidableInstances, InstanceSigs,
             TypeApplications, FlexibleInstances, StandaloneDeriving #-}

module AddrSing where

import GHC.TypeLits
import Data.Kind
import Data.Singletons.TH
import Data.Singletons.Sigma

现在我们可以定义AddrType并为其生成单例：

singletons
  [d| data AddrType = Post | Email | Office
        deriving Show
  |]

到目前为止没有什么幻想，但是我们有了AddrFields，这有点棘手：

data AddrFields :: AddrType -> Type where
  PostFields :: { city :: Symbol, street :: Symbol } -> AddrFields Post
  EmailFields :: { email :: Symbol } -> AddrFields Email
  OfficeFields :: { floor :: Nat, desk :: Nat } -> AddrFields Office

deriving instance Show (AddrFields addrType)

[我不得不使用String和Integer，而不是Symbol和Nat，因为可以提升后者。然后，由于AddrFields本身就是GADT，因此我们必须手动将其单调化：

data SAddrFields :: forall addrType. AddrFields addrType -> Type where
  SPostFields :: Sing city -> Sing street -> SAddrFields (PostFields city street)
  SEmailFields :: Sing email -> SAddrFields (EmailFields email)
  SOfficeFields :: Sing floor -> Sing desk -> SAddrFields (OfficeFields floor desk)

deriving instance Show (SAddrFields addrFields)

type instance Sing = SAddrFields

instance (SingI city, SingI street) => SingI (PostFields city street) where
  sing = SPostFields sing sing

instance (SingI email) => SingI (EmailFields email) where
  sing = SEmailFields sing

instance (SingI floor, SingI desk) => SingI (OfficeFields floor desk) where
  sing = SOfficeFields sing sing

自动执行此位是一个未解决的问题：https://github.com/goldfirere/singletons/issues/150

接下来，让我们定义Addr，它只是一个依赖对：

type Addr = Sigma AddrType (TyCon AddrFields)

这里是Addr值的示例：

x :: Addr
x = SPost :&: PostFields undefined undefined

Symbol的PostFields字段不能有任何居民，因此我不得不用undefined填写他们，但此刻不重要。请注意，我们已经有一个单例作为我们的第一个组件SPost。

这是单身人士发挥作用的地方。我们可以如下单调x：

xSing :: Sing @Addr (SPost :&: PostFields "Foo" "Bar")
xSing = sing

最后一点，让我们定义someCoolPredicate和AddrList：

singletons
  [d|
    someCoolPredicate :: [Addr] -> Bool
    someCoolPredicate (_ : _) = True
    someCoolPredicate [] = False
  |]

data AddrList :: [Addr] -> Type where
  MkAddrList :: (SomeCoolPredicate addrs ~ True) => Sing addrs -> AddrList addrs

deriving instance Show (AddrList addrs)

---

有了这种机器，您的Idris示例MkAddrList [(Post ** PostFields "Foo" "Bar")]编写如下：

ghci> MkAddrList @'[SPost :&: PostFields "Foo" "Bar"] sing
MkAddrList (SCons (SWrapSing {sUnwrapSing = SPost} :&: SPostFields (SSym @"Foo") (SSym @"Bar")) SNil)

此处的完整代码：https://gist.github.com/int-index/743ad7b9fcc54c9602b4eecdbdca34b5