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.