Module

Typelevel.Arithmetic.Add

Package
purescript-typelevel-arithmetic
Repository
sigma-andex/purescript-typelevel-arithmetic

#AddSingle Source

class AddSingle :: Symbol -> Symbol -> Symbol -> Symbol -> Symbol -> Constraintclass AddSingle (augend :: Symbol) (addend :: Symbol) (carryPrevious :: Symbol) (carryNext :: Symbol) (sum :: Symbol) | augend addend carryPrevious -> carryNext sum, augend carryPrevious sum -> addend carryNext, addend carryPrevious sum -> augend carryNext

Class for internal use only. See Add instead. Typeclass for adding two single digits.

Instances

#Add Source

class Add :: Symbol -> Symbol -> Symbol -> Symbol -> Constraintclass Add (augend :: Symbol) (addend :: Symbol) (carry :: Symbol) (sum :: Symbol) | augend addend -> carry sum, augend sum -> addend carry, addend sum -> augend carry

Typeclass for adding two typelevel numbers represented as symbols Note: Currently, the terms have to be equal length. Use the PadZeroes typeclass to align the terms. Use Trim to remove any excessive zeroes after the calculation.

Example usage:

add ∷
  ∀ augend addend sum carry result.
  Add augend addend carry sum ⇒
  Cons carry sum result ⇒
  Proxy augend → Proxy addend → Proxy result
add _ _ = Proxy

result ∷ Proxy "0579"
result = add (term ∷ _ "123") (term ∷ _ "456")

Instances

  • Add "" "" "0" ""
  • (Cons augendHead augendTail augend, Cons addendHead addendTail addend, Cons sumHead sumTail sum, Add augendTail addendTail carryPrevious sumTail, AddSingle augendHead addendHead carryPrevious carry sumHead) => Add augend addend carry sum

#PadZeroesHelper Source

class PadZeroesHelper :: Symbol -> Symbol -> Symbol -> Symbol -> Symbol -> Symbol -> Constraintclass PadZeroesHelper (leftIn :: Symbol) (rightIn :: Symbol) (leftTemp :: Symbol) (rightTemp :: Symbol) (leftOut :: Symbol) (rightOut :: Symbol) | leftIn rightIn leftTemp rightTemp -> leftOut rightOut

Typeclass for internal use only. See PadZeroes instead.

Instances

#PadZeroes Source

class PadZeroes :: Symbol -> Symbol -> Symbol -> Symbol -> Constraintclass PadZeroes (leftIn :: Symbol) (rightIn :: Symbol) (leftOut :: Symbol) (rightOut :: Symbol) | leftIn rightIn -> leftOut rightOut

Typeclass to align two symbols by padding the shorter one with zeroes.

Instances

#TrimHelper Source

class TrimHelper :: Symbol -> Symbol -> Symbol -> Constraintclass TrimHelper (inHead :: Symbol) (inTail :: Symbol) (out :: Symbol) | inHead inTail -> out

Typeclass for internal use only. See Trim instead.

Instances

#Trim Source

class Trim :: Symbol -> Symbol -> Constraintclass Trim (input :: Symbol) (output :: Symbol) | input -> output

Typeclass to trim a symbol by removing any excess zeroes.

Instances

#term Source

term :: forall t. Proxy t

Just an alias for Proxy to make it a bit nicer to read:

term :: _ "123"

instead of

Proxy :: Proxy "123"

#Term Source

type Term :: forall k. k -> Typetype Term sym = Proxy sym