Can the type of a function be constrained to certain promoted data constructors?

Question

I'm trying to wrap my head around promoted data constructors. In particular I was wondering if they are useful in contexts that do not involve type families and GADT's. So I tried to think about whether they could be use to constraint the term level values that a certain function could take. For instance, would it be possible to define a function that accepts only list of all True terms. The following will not work, since (->) is a function from Type to Type and '[ 'True] has kind [Bool]:

allTrue :: '[ 'True] -> Int
allTrue = length 

However I was wondering if one could make use of the promoted data constructor 'True to define such a function. Furthermore, would such definition always require GADT's and/or type-families?

Answer 1

To answer your specific question: no, there is no type whose values are lists containing only True. The promoted constructor 'True is just another type, but because it's not of the kind Type, it doesn't have any values.

To answer your more general question: yes, there is a use of promoted type constructors even without type families and GADTs. Phantom types are types with a type parameter that doesn't appear in its values at all. You can use them to have the type system do some bookkeeping for you. For example, suppose you want to keep track of whether you've escaped HTML in a String, to avoid injection attacks. You can write this:

data IsEscaped = Escaped | NotEscaped

newtype UserText (e :: IsEscaped) = UserText { getUserText :: String }

fromRawUserText :: String -> UserText 'NotEscaped
fromRawUserText = UserText

escape :: UserText 'NotEscaped -> UserText 'Escaped
escape (UserText s) = UserText (escapeHTML s)

You can then export from this module the type UserText, and the functions fromRawUserText, escape, and getUserText, but not the UserText constructor. Now you have a type that keeps track of whether it has been escaped or not. It will be an error to call escape on a String that's already escaped, and also to pass a UserText 'NotEscaped to a function that's expecting a UserText 'Escaped.

You could accomplish the same thing with something like

data NotEscaped
data Escaped
data UserText a = ...

but you lose the type information of knowing that UserText is supposed to be instantiated with Escaped or NotEscaped. So this is, essentially, untyped programming at the type level. Promoted data constructors let you do typed programming at the type level.

Answer 2

You can generally avoid GADTs using higher-rank types, though it will be much, much less convenient.

{-# language RankNTypes, FunctionalDependencies, FlexibleInstances, ScopedTypeVariables #-}
import qualified Control.Category as C
import Data.Functor.Identity

newtype Same a b = Same {unSame :: forall f. f a -> f b}

coerceWith :: Same a b -> a -> b
coerceWith (Same f) = runIdentity . f . Identity

newtype Flip p a b = Flip {unFlip :: p b a}

refl :: Same a a
refl = Same id

sym :: Same a b -> Same b a
sym (Same f) = unFlip . f . Flip $ refl

trans :: Same a b -> Same b c -> Same a c
trans (Same f) (Same g) = Same (g . f)

instance C.Category Same where
  id = refl
  (.) = flip trans

-- Constraint-based sameness

-- The fundeps improve inference
class Sam a b | a -> b, b -> a where
  mas :: f a -> f b
instance Sam a a where
  mas = id

same :: Sam a b => Same a b
same = Same mas

newtype Gum a b = Gum
  { unGum :: forall r. (Sam a b => r) -> r }

withSame :: Same a b -> (Sam a b => r) -> r
withSame (Same s) = unGum $ s (Gum id)

symSam :: forall a b r pa pb. Sam a b => pa a -> pb b -> (Sam b a => r) -> r
symSam _ _ p = withSame (sym same :: Same b a) p

transSam :: forall a b c r pa pb pc. (Sam a b, Sam b c) => pa a -> pb b -> pc c -> (Sam a c => r) -> r
transSam _ _ _ p = withSame (trans (same :: Same a b) (same :: Same b c)) p