Copyright	© Frank Jung 2023
License	GPL-3.0-only
Safe Haskell	Safe-Inferred
Language	Haskell2010

Singletons

Contents

Functions

Description

This is from a talk by Richard Eisenberg about Generalized Abstract Data Types.

Singletons are a useful work-around for dependent types in Haskell. Singletons can be used for:

reflection
reification
promoting function values to become functions on types
defunctionalization (turning functions into data)

A key benefit is the ability to move runtime errors into compile time errors.

Type erasure In Haskell, types only exist at compile-time, for help with type-checking. They are completely erased at runtime.

Resources

From Tweag YouTube channel specifically Richard Eisenberg's series on Haskell.

Returning different types does not work

However, returning different types does not work. For example, one way to define a function that returns different types depending upon the SingT parameter.

But this does not work because the t type is not known at compile time. It should return a type t not a type 'Maybe a' constructor which has no arguments.

one :: SingT t -> t
one SInt       = 1
one SBool      = True
one (SMaybe _) = Just ()

Synopsis

data SingT t where
- SArrow :: SingT a -> SingT b -> SingT (a -> b)
- SBool :: SingT Bool
- SInt :: SingT Int
- SList :: SingT a -> SingT [a]
- SMaybe :: SingT a -> SingT (Maybe a)
- SUnit :: SingT ()
- SWrapper :: SingT a -> SingT (Wrapper a)
newtype Wrapper a = Wrapper {
- getWrapper :: a
}
zero :: SingT t -> t
eqSingT :: SingT t -> SingT t -> Bool
convertViaInt :: (Integral a, Num b) => a -> b

Documentation

data SingT t where Source #

SingT is a example of a Singleton type. This is an indexed type.

This gets compiled as:

data SingT t
  = (t ~ Int) => SInt
  | (t ~ Bool) => SBool
  | forall a. (t ~ Maybe a) => SMaybe (SingT a)
  | forall a. (t ~ [a]) => SList (SingT a)
  | (t ~ ()) => SUnit
  | forall a b. (t ~ (a -> b)) => SArrow (SingT a) (SingT b)
  | forall a. (t ~ Wrapper a) => SWrapper (SingT a)

Constructors

SArrow :: SingT a -> SingT b -> SingT (a -> b)
SBool :: SingT Bool
SInt :: SingT Int
SList :: SingT a -> SingT [a]
SMaybe :: SingT a -> SingT (Maybe a)
SUnit :: SingT ()
SWrapper :: SingT a -> SingT (Wrapper a)

Instances

Instances details

Show (SingT t) Source #
Instance details Defined in Singletons Methods showsPrec :: Int -> SingT t -> ShowS # show :: SingT t -> String # showList :: [SingT t] -> ShowS #

newtype Wrapper a Source #

A very simple newtype wrapper.

Constructors

Wrapper
Fields getWrapper :: a

Instances

Instances details

Show a => Show (Wrapper a) Source #
Instance details Defined in Singletons Methods showsPrec :: Int -> Wrapper a -> ShowS # show :: Wrapper a -> String # showList :: [Wrapper a] -> ShowS #

Functions

zero :: SingT t -> t Source #

Zero: This function can return difference types, depending upon the SingT parameter.

Examples

>>> zero SInt
0
>>> zero SWrapper SBool
False
>>> zero (SMaybe SInt)
Nothing

eqSingT :: SingT t -> SingT t -> Bool Source #

Define equality for each Singleton type.

convertViaInt :: (Integral a, Num b) => a -> b Source #

Example of specified and inferred types. This is from "Effective Haskell, Specified and Inferred Types" by Rebecca Skinner.

Explanation

When the type is specified in the signature, then we have un-bracketed terms:

λ>  :set -fprint-explicit-foralls
λ> :t convertViaInt
convertViaInt :: forall a b. (Integral a, Num b) => a -> b

However, when the type is inferred, then we have bracketed terms: (Inferred when the type is not specified in the signature.)

λ> :t convertViaInt
convertViaInt :: forall {a} {b}. (Integral a, Num b) => a -> b

You can mix these two styles:

λ> :set -XTypeApplications
λ> :set -XExplicitForAll
convertViaInt :: forall {a} b. (Integral a, Num b) => a -> b
convertViaInt x = fromIntegral $ fromIntegral _ Int x

λ> :t convertViaInt @Double 100
100.0