snumber


Keywords
constraints, library, Propose Tags
License
Apache-2.0
Install
cabal install snumber-0.2.0

Documentation

dependent-literals

Pseudo-dependently-typed integral literals for Haskell.

Stack CI

Disclaimer

This is not an officially supported Google product.

Hackage Status

  • numeric-kinds Uploaded Haddock
  • snumber Uploaded Haddock
  • dependent-literals Uploaded Haddock
  • dependent-literals-plugin Uploaded Haddock

Overview

This repository contains several packages implementing pseudo-dependently-typed integral literals in GHC Haskell.

In standard Haskell, integer literals 42 are interpreted under the hood as a call to the Num method fromInteger 42 :: Num a => a. This means the type is determined solely by the context, and any failures of bounds checking can be observed only at runtime. This plugin replaces that mechanism with one that reflects the literal's value to the type level, and allows instances to refine the resulting type and perform type-level bounds checks according to the value of the literal.

For example, given mkVec :: SInt n -> (Fin n -> a) -> Vec n a, mkVec 4 will have type (Fin 4 -> a) -> Vec 4 a, and trying to type-check 4 :: Fin 4 will report a type error saying that 4 is out of range.

Patterns get a similar treatment, too, so case (x :: SInt n) of { 1 -> Just Refl; _ -> Nothing } :: Maybe (n :~: 1) can type-check: the act of matching against 1 proved that the type-level n was equal to 1.