symantic-6.3.0.20170807: Library for Typed Tagless-Final Higher-Order Composable DSL

Safe HaskellSafe
LanguageHaskell2010

Language.Symantic.Typing.Peano

Contents

Description

Natural numbers inductivey defined at the type-level, and of kind *.

Synopsis

Types Zero and Succ

data Zero Source #

Instances

IPeano Zero Source # 
SymInjP k * Zero ((:) * (Proxy k s) ss) s Source # 

Methods

symInjP :: TeSym ((* ': Proxy Zero s) [*]) ts t -> TeSym ss ts t Source #

data Succ p Source #

Instances

SymInjP k1 * p ss s => SymInjP k1 * (Succ p) ((:) * (Proxy k not_s) ss) s Source # 

Methods

symInjP :: TeSym ((* ': Proxy (Succ p) s) [*]) ts t -> TeSym ss ts t Source #

IPeano p => IPeano (Succ p) Source # 

Methods

ipeano :: SPeano (Succ p) Source #

Type synonyms for a few numbers

type P0 = Zero Source #

type P1 = Succ P0 Source #

type P2 = Succ P1 Source #

type P3 = Succ P2 Source #

Type SPeano

data SPeano p where Source #

Singleton for Zero and Succ.

Constructors

SZero :: SPeano Zero 
SSucc :: SPeano p -> SPeano (Succ p) 

Instances

TestEquality * SPeano Source # 

Methods

testEquality :: f a -> f b -> Maybe ((SPeano :~: a) b) #

Type IPeano

class IPeano p where Source #

Implicit construction of SPeano.

Minimal complete definition

ipeano

Methods

ipeano :: SPeano p Source #

Instances

Type EPeano

data EPeano where Source #

Constructors

EPeano :: SPeano p -> EPeano 

Instances

Interface with Integral

peano_from_integral :: Integral i => i -> (forall p. SPeano p -> ret) -> ret Source #