将存在主义提升到类型级别

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

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

我在现代 Haskell 中设法实现的最接近的是，假设单例 2.5：

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

但是我如何实际构造一个给定的这种类型的值[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)

我必须使用Stringand代替and ，因为后者可以升级。然后，由于它本身是一个 GADT，我们必须手动将其单例化：IntegerSymbolNatAddrFields

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