Singletons of singletons (emulating complex pi types in Haskell)

Question

I've got a simple proof of concept in Idris which uses dependent types to enforce some not-too-complex business logic. A few names have been changed to protect the not-so-innocent, but the idea is that we want to collect "lines" in a sequence. Each line pertains to a specific section, but only one (EconProduction) has anything we care about yet. In general, lines have a section-specific keyword and an expression whose form/type may depend upon the keyword used.

For this particular section, each line either describes some numbers for a "phase" (Prod), or continues the last named "phase" (Continue).

In Idris, we can do this like so:

data EconSection
  = EconGeneral
  | EconProduction

data EconPhase
  = Oil
  | Water
  | NumPhase Nat

data ContState
  = ContNone
  | ContProd EconPhase

data Keyword : EconSection -> ContState -> ContState -> Type where
  Prod : (p : EconPhase) -> Keyword EconProduction c (ContProd p)
  Continue : Keyword s c c

data Expression : (s : EconSection) ->
                  (d : ContState) ->
                  Keyword s c d ->
                  Type where
  ExProc : Double -> Double -> Expression EconProduction (ContProd p) k

data Line : EconSection -> ContState -> ContState -> Type where
  L : (k : Keyword s c d) -> Expression s d k -> Line s c d

data Lines : EconSection -> ContState -> Type where
  First : Line s ContNone d -> Lines s d
  Then : Lines s c -> Line s c d -> Lines s d

infixl 0 `Then`

good : Lines EconProduction (ContProd (NumPhase 1))
good = First (L (Prod Oil) (ExProc 23.2 70.1))
      `Then` (L (Continue) (ExProc 27.9 1.2))
      `Then` (L (Prod (NumPhase 1)) (ExProc 91.2 7014.1))
      `Then` (L (Continue) (ExProc 91.2 7014.1))

So far so good! The usual dependent typestate business. For eminently practical business reasons, we wish to actually implement this logic in GHC Haskell. I've built it with singletons (rolled my own as-needed rather than use the singletons package, just for a short proof of concept):

{-# LANGUAGE GADTs, KindSignatures, DataKinds #-}
{-# LANGUAGE RankNTypes, TypeInType, TypeOperators #-}
{-# LANGUAGE TypeFamilies, TypeFamilyDependencies, MultiParamTypeClasses #-}

import Data.Kind (Type)

data Nat
  = Z
  | S Nat

data SNat :: Nat -> Type where
  SZ :: SNat 'Z
  SS :: SNat n -> SNat ('S n)

data SSNat :: forall (n :: Nat) . SNat n -> Type where
  SSZ :: SSNat 'SZ
  SSS :: SSNat n -> SSNat ('SS n)

type family SingNat (n :: Nat) :: SNat n where
  SingNat 'Z = 'SZ
  SingNat ('S n) = 'SS (SingNat n)

data EconSection
  = EconGeneral
  | EconProduction

data SEconSection :: EconSection -> Type where
  SEconGeneral :: SEconSection 'EconGeneral
  SEconProduction :: SEconSection 'EconProduction

type family SingSection (s :: EconSection) :: SEconSection s where
  SingSection 'EconGeneral = 'SEconGeneral
  SingSection 'EconProduction = 'SEconProduction 

data EconPhase
  = Oil
  | Water
  | NumPhase Nat

data SEconPhase :: EconPhase -> Type where
  SOil :: SEconPhase 'Oil
  SWater :: SEconPhase 'Water
  SNumPhase :: SNat n -> SEconPhase ('NumPhase n)

data SSEconPhase :: forall (p :: EconPhase) . SEconPhase p -> Type where
  SSOil :: SSEconPhase 'SOil
  SSWater :: SSEconPhase 'SWater
  SSNumPhase :: SSNat n -> SSEconPhase ('SNumPhase n)

type family SingEconPhase (p :: EconPhase) :: SEconPhase p where
  SingEconPhase 'Oil = 'SOil
  SingEconPhase 'Water = 'SWater
  SingEconPhase ('NumPhase n) = 'SNumPhase (SingNat n)

data ContState
  = ContNone
  | ContProd EconPhase

data SContState :: ContState -> Type where
  SContNone :: SContState 'ContNone
  SContProd :: SEconPhase p -> SContState ('ContProd p)

type family SingContState (c :: ContState) :: SContState c where
  SingContState 'ContNone = 'SContNone
  SingContState (ContProd p) = 'SContProd (SingEconPhase p)

data Keyword :: EconSection -> ContState -> ContState -> Type where
  Prod :: SEconPhase p -> Keyword 'EconProduction c ('ContProd p)
  Continue :: Keyword s c c

data SKeyword :: forall (s :: EconSection) (c :: ContState) (d :: ContState) .
                 Keyword s c d -> Type where
  SProd :: SSEconPhase p -> SKeyword ('Prod p)
  SContinue :: SKeyword 'Continue

data Expression :: forall (s :: EconSection) (c :: ContState) (d :: ContState) .
                   SEconSection s -> SContState d -> Keyword s c d -> Type where
  ExProc :: Double -> Double -> Expression SEconProduction (SContProd p) k

type family KWSection k where
  KWSection (Keyword s _ _) = s

type family KWFrom k where
  KWFrom (Keyword _ c _) = c

type family KWTo k where
  KWTo (Keyword _ _ d) = d

data Line :: EconSection -> ContState -> ContState -> Type where
  L :: SKeyword (k :: Keyword s c d)
    -> Expression (SingSection s) (SingContState d) k
    -> Line s c d

data Lines :: EconSection -> ContState -> Type where
  First :: Line s 'ContNone d -> Lines s d
  Then :: Lines s c -> Line s c d -> Lines s d

infixl 0 `Then`

good :: Lines 'EconProduction ('ContProd ('NumPhase ('S 'Z)))
good = First (L (SProd SSOil) (ExProc 23.2 70.1))
      `Then` (L (SContinue) (ExProc 27.9 1.2))
      `Then` (L (SProd (SSNumPhase (SSS SSZ))) (ExProc 91.2 7014.1))
      `Then` (L (SContinue) (ExProc 91.2 7014.1))

Here's my question. Is there any way to avoid the "singletons of singletons"? I don't like the look of things like SSNat and so on at all, but this is where I get by translating every pi type to an extra layer of singleton-ing. I haven't been able to make any simpler approach work, and I've not seen any clever ideas in the singletons package to make this easier, though I might have easily missed something beneath all the Template Haskell.

Answer 1

Yes.

Consider that, by the definition of a singleton type, you have as much type information in a singleton as the singleton of that singleton, because they both have a unique instance.

In your code

With the above in mind, we can remove the SSNat and SSEconPhase declarations from your code. Then, in the SProd constructor

SProd :: SSEconPhase p - > SKeyword ('Prod p)

We know that SEconPhase would be sufficient to decide p, so we can rewrite it as

SProd :: SEconPhase p - > SKeyword ('Prod p)

Which produces a kind error - what we need is a type transformation like

SomeType :: (p :: EconPhase) -> SEconPhase p

Which you already have defined in your code as SingEconPhase. The result is

SProd :: SEconPhase p - > SKeyword ('Prod (SingEconPhase p))

In general

You should never have to write a singleton of a singleton - if you need to "lift" a type parameter to the singleton type, then the correct choice is to write a type family as you have done.