typenums: Type level numbers using existing Nat functionality

[ bsd3, data, library ] [ Propose Tags ]

Type level numbers using existing Nat functionality. Uses kind-polymorphic typeclasses and type families to facilitate more general code compatible with existing code using type-level Naturals.


[Skip to Readme]

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

Versions [RSS] 0.1.0.0, 0.1.1, 0.1.1.1, 0.1.2, 0.1.2.1, 0.1.3, 0.1.4 (info)
Change log CHANGELOG.md
Dependencies base (>=4.10 && <5.0) [details]
License BSD-3-Clause
Copyright 2018-2021 Iris Ward
Author AdituV
Maintainer aditu.venyhandottir@gmail.com
Category Data
Home page https://github.com/adituv/typenums#readme
Bug tracker https://github.com/adituv/typenums/issues
Source repo head: git clone https://github.com/adituv/typenums
Uploaded by AdituV at 2021-03-23T00:00:42Z
Distributions LTSHaskell:0.1.4, NixOS:0.1.4, Stackage:0.1.4
Reverse Dependencies 1 direct, 0 indirect [details]
Downloads 4840 total (35 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs available [build log]
Last success reported on 2021-03-23 [all 1 reports]

Readme for typenums-0.1.4

[back to package description]

typenums

Hackage example workflow BSD3 license

Type level numbers using existing Nat functionality. Uses kind-polymorphic typeclasses and type families to facilitate more general code compatible with existing code using type-level Naturals.

Usage

Import either Data.TypeNums or Data.TypeLits instead of GHC.TypeLits. Some definitions conflict with GHC.TypeLits, so if you really must import it, use an explicit import list.

This library is intended to be used in a kind-polymorphic way, such that a type-level integer parameter can be written as a natural, and a rational can be written as either of the other two. As an example:

{-# LANGUAGE PolyKinds #-}

data SomeType (n :: k) = SomeType

useSomeType :: KnownInt n => SomeType n -> _
useSomeType = -- ...

Syntax

  • Positive integers are written as natural numbers, as before. Optionally they can also be written as Pos n.
  • Negative integers are written as Neg n.
  • Ratios are written as n :% d, where n can be a natural number, Pos n, or Neg n, and d is a natural number.

Addition, subtraction and multiplication at type level are all given as infix operators with standard notation, and are compatible with any combination of the above types. Equality and comparison constraints are likewise available for any combination of the above types.

N.B. The equality constraint conflicts with that in Data.Type.Equality. The (==) operator from Data.Type.Equality is re-exported as (==?) from both Data.TypeNums and Data.TypeLits.