Skip to content

Instantly share code, notes, and snippets.

@keksnicoh
Last active October 31, 2020 16:21
Show Gist options
  • Save keksnicoh/f49c7c8d3938a81f32385c997c249ea6 to your computer and use it in GitHub Desktop.
Save keksnicoh/f49c7c8d3938a81f32385c997c249ea6 to your computer and use it in GitHub Desktop.
Singletons - Dependent Pair
-- 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
-- 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment