Lifting existentials to type level

Question

tl;dr: I'm trying to rewrite some dependently-typed code that has a list of sigma-types in Haskell, and I can't seem to generate singletons for an existential, in other words this code fails:

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

$(genSingletons [''Foo])

Longer version follows.

Assume this Idris code as a model:

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

Basically, when we're given a value of type AddrList lst, we know that lst : List Addr, and that someCoolPredicate holds for that list.

The closest I managed to achieve in modern Haskell is, assuming 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

But how do I actually construct a value of this type given an [Addr]? In other words, how do I express something like the following in Idris?

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

The problem is that looks like I have to be able to do toSing or equivalent on the list of Addr, but $(genSingletons [''Addr]) fails. Indeed, even the code in the tl;dr section fails. So what should I do, except for abandoning this idea?

int_index int_index · Accepted Answer · 2020-01-24T20:26:11

The solution to this problem requires singletons of singletons, which were introduced in singletons-2.6. First, the required language extensions and imports:

{-# 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

Now we can define AddrType and generate singletons for it:

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

Nothing fancy so far, but then we have AddrFields, which is a bit more tricky:

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)

Instead of String and Integer I had to use Symbol and Nat, as the latter can be promoted. And then, since AddrFields is itself a GADT, we have to singletonize it by hand:

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

Automating this bit is an open issue: https://github.com/goldfirere/singletons/issues/150

Next, let's define Addr, which is simply a dependent pair:

type Addr = Sigma AddrType (TyCon AddrFields)

Here's an example of an Addr value:

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

The Symbol fields of PostFields cannot have any inhabitants, so I had to fill them in with undefined, but this is unimportant at the moment. Just note that we already have a singleton as our first component, SPost.

This is where singletons of singletons come into play. We can singletonize x as follows:

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

For the final bit, let's define someCoolPredicate and 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)

With this machinery in place, your Idris example MkAddrList [(Post ** PostFields "Foo" "Bar")] is written as follows:

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

Full code here: https://gist.github.com/int-index/743ad7b9fcc54c9602b4eecdbdca34b5

Lifting existentials to type level

1 Answers