DTExample.hs

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE DataKinds #-}

module DTExample where

import Data.Singletons
import Data.Singletons.TH

import GHC.TypeLits

data AddressType = Private | Business

genSingletons [''AddressType]

type family AddressParts (a :: AddressType) :: * where
  AddressParts Private = String -- Don't need an address
  AddressParts Business = ( String
                          , Int -- e.g. House number
                          ) -> String

makeAddress :: forall (at :: AddressType). Sing at -> AddressParts at
makeAddress at =
  case at of
    SPrivate -> "No address"
    SBusiness -> \ (address, number) -> address ++ " #" ++  show number


test1 = makeAddress SPrivate
-- >>> "No address"

test3 = makeAddress SBusiness ("business1", 17)
-- "business1 #17"