Singletons - Dependent Pair

Sigma.hs

-- this is using template haskell to reduce boilerplate
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TemplateHaskell #-}

module SigmaCustomSing where

import Data.Singletons.Sigma (Sigma (..))
import Data.Singletons.TH (genDefunSymbols, genSingletons)

data Label
  = LA
  | LB
  | LC
  deriving (Show, Eq)

genSingletons [''Label]

type family LabelIndex (k :: Label) where
  LabelIndex LA = String
  LabelIndex LB = Int
  LabelIndex LC = Int

$(genDefunSymbols [''LabelIndex])

f :: Sigma Label LabelIndexSym0 -> String
f (SLA :&: s) = s
f (SLB :&: i) = show i
f (SLC :&: s) = show s

SigmaBoilerplate.hs

-- expanded version to understand the underlying mechanics
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}

module SigmaBoilerplate where

import Data.Kind (Type)
import Data.Singletons

-- dependent pair: the type of the second element depends on the value of the first
--
-- (s :: Type) : type of the first element
-- (s ~> Type) : type indexed by the first element's type s
--               (~>: see below for defunctionalization)
data Sigma (s :: Type) :: (s ~> Type) -> Type where
  (:&:) :: Sing (fst :: s) -> Apply t fst -> Sigma s t

--         Sing ('LA :: Label)
--                            Apply LabelSym 'LA = String
--                                           Sigma Label LabelSym

data Label
  = LA
  | LB
  | LC
  deriving (Show, Eq)

data SLabel :: Label -> Type where
  SLA :: SLabel LA
  SLB :: SLabel LB
  SLC :: SLabel LC

instance Show (SLabel a) where
  show SLA = "SLA"
  show SLB = "SLB"
  show SLC = "SLC"

type instance Sing = SLabel

instance SingKind Label where
  type Demote Label = Label

  toSing LA = SomeSing SLA
  toSing LB = SomeSing SLB
  toSing LC = SomeSing SLC

  fromSing = \case
    SLA -> LA
    SLB -> LB
    SLC -> LC

type family LabelIndex (k :: Label) :: Type where
  LabelIndex LA = String
  LabelIndex LB = Int
  LabelIndex LC = Int

-- trick: encode type-level function as a type constructor
data LabelSym :: (TyFun Label Type) -> Type

-- type constructors can be applied partially
-- ...               are injective and generative

type instance Apply LabelSym x = LabelIndex x

h :: Sigma Label LabelSym -> String
h (SLA :&: s) = s
h (SLB :&: i) = show i
h (SLC :&: s) = show s