The inch package

[Tags: bsd3, program]

Inch is a type-checker for a subset of Haskell (plus some GHC extensions) with the addition of integer constraints. After successfully type-checking a source file, it outputs an operationally equivalent version with the type-level integers erased, so it can be used as a preprocessor in order to compile programs.


[Skip to ReadMe]

Properties

Versions0.1.0, 0.2.0
Change logNone available
Dependenciesbase (==4.*), containers (>0.4 && <0.6), filepath (>1.2 && <1.4), IndentParser (>0.2 && <0.3), mtl (>2.0 && <2.3), parsec (>3.1 && <3.5), presburger (==0.4.*), pretty (>=1.0 && <2) [details]
LicenseBSD3
CopyrightCopyright (c) 2011 Adam Gundry
AuthorAdam Gundry <adam.gundry@strath.ac.uk>
MaintainerAdam Gundry <adam.gundry@strath.ac.uk>
CategoryLanguage
Home pagehttps://github.com/adamgundry/inch/
Bug trackerhttps://github.com/adamgundry/inch/issues
Source repositoryhead: git clone git://github.com/adamgundry/inch.git
Executablesinch
UploadedSat Jun 7 14:44:25 UTC 2014 by AdamGundry
Downloads348 total (19 in last 30 days)
Votes
0 []
StatusDocs not available [build log]
Last success reported on 2015-05-20 [all 2 reports]

Downloads

Maintainers' corner

For package maintainers and hackage trustees

Readme for inch-0.2.0

inch

Inch is a type-checker for a subset of Haskell (plus some GHC extensions) with the addition of integer constraints. After successfully type-checking a source file, it outputs an operationally equivalent version with the type-level integers erased, so it can be used as a preprocessor in order to compile programs.

This is a very rough and ready prototype. Many Haskell features are missing or poorly implemented.

Installation

cabal install inch

Features

Example

The following program defines a type of vectors (lists indexed by their length) and some functions using them.

{-# OPTIONS_GHC -F -pgmF inch #-}
{-# LANGUAGE RankNTypes, GADTs, KindSignatures, ScopedTypeVariables, NPlusKPatterns #-}

data Vec :: * -> Nat -> * where
    VNil  :: Vec a 0
    VCons :: forall a (n :: Nat) . a -> Vec a n -> Vec a (n+1)
  deriving Show

vreverse :: forall (n :: Nat) a . Vec a n -> Vec a n
vreverse xs = vrevapp xs VNil
  where
    vrevapp :: forall (m n :: Nat) a . Vec a m -> Vec a n -> Vec a (m+n)
    vrevapp VNil         ys = ys
    vrevapp (VCons x xs) ys = vrevapp xs (VCons x ys)

vec :: pi (n :: Nat) . a -> Vec a n
vec {0}   a = VNil
vec {n+1} a = VCons a (vec {n} a)

vlookup :: forall (n :: Nat) a . pi (m :: Nat) . m < n => Vec a n -> a
vlookup {0}   (VCons x _)  = x
vlookup {k+1} (VCons _ xs) = vlookup {k} xs

plan :: pi (n :: Nat) . Vec Integer n
plan {0}           = VNil
plan {m} | {m > 0} = VCons m (plan {m-1})

After type-checking and preprocecessing with inch, the resulting file is as follows.

{-# LANGUAGE RankNTypes, GADTs, KindSignatures, ScopedTypeVariables, NPlusKPatterns #-}

data Vec :: * -> * where
    VNil  :: Vec a
    VCons :: a -> Vec a -> Vec a
  deriving Show

vreverse :: Vec a -> Vec a
vreverse xs = vrevapp xs VNil
  where
    vrevapp :: Vec a -> Vec a -> Vec a
    vrevapp VNil         ys = ys
    vrevapp (VCons x xs) ys = vrevapp xs (VCons x ys)

vec :: Integer -> a -> Vec a n
vec 0     a = VNil
vec (n+1) a = VCons a (vec n a)

vlookup :: Integer -> Vec a n -> a
vlookup 0     (VCons x _)  = x
vlookup (k+1) (VCons _ xs) = vlookup k xs

plan :: Integer -> Vec Integer
plan 0         = VNil
plan m | m > 0 = VCons m (plan (m-1))

For more examples, look in the examples directory of the source distribution. These include:

Known limitations

Outstanding design issues

Related work

Iavor Diatchki is working on TypeNats, an extension to GHC that aims to support type-level natural numbers. He also implemented the presburger package, which inch uses for constraint solving.

Conor McBride's Strathclyde Haskell Enhancement is a preprocessor that supports Π-types and allows lifting algebraic data types (but not numeric types) to kinds. SHE inspired the braces syntax used in inch. These ideas (and more, including kind polymorphism) are being implemented in GHC: see Giving Haskell a Promotion by Brent Yorgey, Stephanie Weirich, Julien Cretin, Simon Peyton Jones and Dimitrios Vytiniotis.

Max Bolingbroke has implemented the new Constraint kind in GHC. This kind is supported by inch but not erased, so it will only work if GHC support is present.

This work is inspired by Hongwei Xi's Dependent ML and its successor ATS, which support type-level Presburger arithmetic.

Contact

Adam Gundry, adam.gundry@strath.ac.uk