Skip to content

Commit

Permalink
Add experimental implementation
Browse files Browse the repository at this point in the history
  • Loading branch information
hvr committed Jan 18, 2014
1 parent ee30ee3 commit d1f8e84
Show file tree
Hide file tree
Showing 6 changed files with 540 additions and 0 deletions.
2 changes: 2 additions & 0 deletions .gitignore
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
*~
/dist/
295 changes: 295 additions & 0 deletions Data/IntCast.hs
Original file line number Diff line number Diff line change
@@ -0,0 +1,295 @@
{-# LANGUAGE CPP, DataKinds, TypeFamilies, TypeOperators, UndecidableInstances #-}

#if __GLASGOW_HASKELL__ < 707
#error This code requires GHC 7.7+
#endif

#include "MachDeps.h"
#include "HsBaseConfig.h"

-- |
-- Module: Data.IntCast
-- Copyright: © 2014 Herbert Valerio Riedel
-- License: BSD-style (see the LICENSE file)
--
-- Maintainer: Herbert Valerio Riedel <hvr@gnu.org>
-- Stability: experimental
-- Portability: GHC ≥ 7.8
--
-- This module provides for statically or dynamically checked
-- conversions between 'Integral' types.
module Data.IntCast
( -- * Conversion functions
-- ** statically checked
intCast
, intCastIso
, intCastEq
-- ** dynamically checked
, intCastMaybe

-- * Registering new integer types
-- |
-- * For 'intCastMaybe' you need to provide type-class instances of 'Bits'
-- (and 'Integral').
--
-- * For 'intCast', 'intCastIso', and 'intCastEq' simply
-- declare instances for the 'IntBaseType' type-family (as well
-- as type-class instances of 'Integral') as described below.
, IntBaseType
, IntBaseTypeK(..)

-- * Type-level predicates
-- | The following type-level predicates are used by 'intCast',
-- 'intCastIso', and 'intCastEq' respectively.
, IsIntSubType
, IsIntBaseSubType
, IsIntTypeIso
, IsIntBaseTypeIso
, IsIntTypeEq
, IsIntBaseTypeEq
) where

-- Haskell 2010+
import Data.Int
import Data.Word
import Foreign.C.Types

-- non-Haskell 2010
import GHC.TypeLits
import Data.Bits

-- | (Kind) Meta-information about integral types.
--
-- If also a 'Bits' instance is defined, the type-level information
-- provided by 'IntBaseType' ought to match the meta-information that
-- is conveyed by the 'Bits' class' 'isSigned' and 'bitSizeMaybe'
-- methods.
data IntBaseTypeK
-- | fixed-width /n/-bit integers with value range [-2ⁿ⁻¹, 2ⁿ⁻¹-1].
= FixedIntTag Nat
-- | fixed-width /n/-bit integers with value range [0, 2ⁿ-1].
| FixedWordTag Nat
-- | integers with value range ]-∞,+∞[.
| BigIntTag
-- | naturals with value range [0,+∞[.
| BigWordTag

-- | The (open) type family 'IntBaseType' encodes type-level
-- information about the value range of an integral type.
--
-- This module also provides type family instances for the standard
-- Haskell 2010 integral types (including "Foreign.C.Types").
--
-- Here's a simple example for registering a custom type with the
-- "Data.IntCast" facilities:
--
-- @
-- /-- user-implemented unsigned 4-bit integer/
-- data Nibble = …
--
-- /-- declare meta-information/
-- type instance 'IntBaseType' MyWord7 = 'FixedIntTag' 4
--
-- /-- user-implemented signed 7-bit integer/
-- data MyInt7 = …
--
-- /-- declare meta-information/
-- type instance 'IntBaseType' MyWord7 = 'FixedIntTag' 7
-- @
--
-- The type-level predicate 'IsIntSubType' provides a partial
-- ordering based on the types above. See also 'intCast'.
type family IntBaseType a :: IntBaseTypeK

type instance IntBaseType Integer = BigIntTag

-- Haskell2010 Basic fixed-width Integer Types
type instance IntBaseType Int8 = FixedIntTag 8
type instance IntBaseType Int16 = FixedIntTag 16
type instance IntBaseType Int32 = FixedIntTag 32
type instance IntBaseType Int64 = FixedIntTag 64
type instance IntBaseType Word8 = FixedWordTag 8
type instance IntBaseType Word16 = FixedWordTag 16
type instance IntBaseType Word32 = FixedWordTag 32
type instance IntBaseType Word64 = FixedWordTag 64

#if defined(WORD_SIZE_IN_BITS)
type instance IntBaseType Int = FixedIntTag WORD_SIZE_IN_BITS
type instance IntBaseType Word = FixedWordTag WORD_SIZE_IN_BITS
#else
#error Cannot determine bit-size of 'Int'/'Word' type
#endif

-- Haskell2010 FFI Integer Types
type instance IntBaseType CChar = IntBaseType HTYPE_CHAR
type instance IntBaseType CInt = IntBaseType HTYPE_INT
type instance IntBaseType CIntMax = IntBaseType HTYPE_INTMAX_T
type instance IntBaseType CIntPtr = IntBaseType HTYPE_INTPTR_T
type instance IntBaseType CLLong = IntBaseType HTYPE_LONG_LONG
type instance IntBaseType CLong = IntBaseType HTYPE_LONG
type instance IntBaseType CPtrdiff = IntBaseType HTYPE_PTRDIFF_T
type instance IntBaseType CSChar = IntBaseType HTYPE_SIGNED_CHAR
type instance IntBaseType CShort = IntBaseType HTYPE_SHORT
type instance IntBaseType CSigAtomic = IntBaseType HTYPE_SIG_ATOMIC_T
type instance IntBaseType CSize = IntBaseType HTYPE_SIZE_T
type instance IntBaseType CUChar = IntBaseType HTYPE_UNSIGNED_CHAR
type instance IntBaseType CUInt = IntBaseType HTYPE_UNSIGNED_INT
type instance IntBaseType CUIntMax = IntBaseType HTYPE_UINTMAX_T
type instance IntBaseType CUIntPtr = IntBaseType HTYPE_UINTPTR_T
type instance IntBaseType CULLong = IntBaseType HTYPE_UNSIGNED_LONG_LONG
type instance IntBaseType CULong = IntBaseType HTYPE_UNSIGNED_LONG
type instance IntBaseType CUShort = IntBaseType HTYPE_UNSIGNED_SHORT

-- Internal class providing the partial order of (improper) subtype-relations
type family IsIntBaseSubType a b :: Bool where
-- this relation is reflexive
IsIntBaseSubType a a = True

-- Every integer is a subset of 'Integer'
IsIntBaseSubType a BigIntTag = True

-- Even though Haskell2010 doesn't provide naturals, we can use the
-- tag 'Nat' to denote such entities
IsIntBaseSubType (FixedWordTag a) BigWordTag = True

-- sub-type relations between fixed-with types
IsIntBaseSubType (FixedIntTag a) (FixedIntTag b) = a <=? b
IsIntBaseSubType (FixedWordTag a) (FixedWordTag b) = a <=? b
IsIntBaseSubType (FixedWordTag a) (FixedIntTag b) = a+1 <=? b

-- everything else is not a sub-type
IsIntBaseSubType a b = False

type IsIntSubType a b = IsIntBaseSubType (IntBaseType a) (IntBaseType b)

-- Same bit-size predicate
type family IsIntBaseTypeIso a b :: Bool where
IsIntBaseTypeIso (FixedIntTag n) (FixedIntTag n) = True
IsIntBaseTypeIso (FixedIntTag n) (FixedWordTag n) = True
IsIntBaseTypeIso (FixedWordTag n) (FixedIntTag n) = True
IsIntBaseTypeIso (FixedWordTag n) (FixedWordTag n) = True
IsIntBaseTypeIso a b = False

type IsIntTypeIso a b = IsIntBaseTypeIso (IntBaseType a) (IntBaseType b)

type family IsIntBaseTypeEq a b :: Bool where
IsIntBaseTypeEq (FixedIntTag n) (FixedIntTag n) = True
IsIntBaseTypeEq (FixedWordTag n) (FixedWordTag n) = True
IsIntBaseTypeEq BigIntTag BigIntTag = True
IsIntBaseTypeEq BigWordTag BigWordTag = True
IsIntBaseTypeEq a b = False

type IsIntTypeEq a b = IsIntBaseTypeEq (IntBaseType a) (IntBaseType b)

-- | Statically checked integer conversion which satisfies the property
--
-- * @'toInteger' ≡ 'toInteger' . intCast@
--
-- Note: This is just a type-restricted alias of 'fromIntegral' and
-- should therefore lead to the same compiled code as if
-- 'fromIntegral' had been used instead of 'intCast'.
intCast :: (Integral a, Integral b, IsIntSubType a b ~ True) => a -> b
intCast = fromIntegral
{-# INLINE intCast #-}

-- | Statically checked integer conversion which satisfies the properties
--
-- * @∀β . 'intCastIso' ('intCastIso' a ∷ β) == a@
--
-- * @'toInteger' ('intCastIso' a) == 'toInteger' b (__if__ 'toInteger' a == 'toInteger' b)@
--
-- Note: This is just a type-restricted alias of 'fromIntegral' and
-- should therefore lead to the same compiled code as if
-- 'fromIntegral' had been used instead of 'intCast'.
intCastIso :: (Integral a, Integral b, IsIntTypeIso a b ~ True) => a -> b
intCastIso = fromIntegral
{-# INLINE intCastIso #-}

-- | Version of 'intCast' restricted to casts between types with same value domain.
intCastEq :: (Integral a, Integral b, IsIntTypeEq a b ~ True) => a -> b
intCastEq = fromIntegral
{-# INLINE intCastEq #-}

----------------------------------------------------------------------------
----------------------------------------------------------------------------
-- dynamically checked conversion

-- | 'Bits' class based value-level predicate with same semantics as 'IsIntSubType'
isBitSubType :: (Bits a, Bits b) => a -> b -> Bool
isBitSubType _x _y
-- reflexive
| xWidth == yWidth, xSigned == ySigned = True

-- Every integer is a subset of 'Integer'
| ySigned, Nothing == yWidth = True
| not xSigned, not ySigned, Nothing == yWidth = True

-- sub-type relations between fixed-with types
| xSigned == ySigned, Just xW <- xWidth, Just yW <- yWidth = xW <= yW
| not xSigned, ySigned, Just xW <- xWidth, Just yW <- yWidth = xW < yW

| otherwise = False
where
xWidth = bitSizeMaybe _x
xSigned = isSigned _x

yWidth = bitSizeMaybe _y
ySigned = isSigned _y
{-# INLINE isBitSubType #-}

-- | Run-time-checked integer conversion
--
-- This is an optimized version of the following generic code below
--
-- > intCastMaybeRef :: (Integral a, Integral b) => a -> Maybe b
-- > intCastMaybeRef x
-- > | toInteger x == toInteger y = Just y
-- > | otherwise = Nothing
-- > where
-- > y = fromIntegral x
--
-- The code above is rather inefficient as it needs to go via the
-- 'Integer' type. The function 'intCastMaybe', however, is marked @INLINEABLE@ and
-- if both integral types are statically known, GHC will be able
-- optimize the code signficantly (for @-O1@ and better).
--
-- For instance (as of GHC 7.8.1) the following definitions
--
-- > w16_to_i32 = intCastMaybe :: Word16 -> Maybe Int32
-- >
-- > i16_to_w16 = intCastMaybe :: Int16 -> Maybe Word16
--
-- are translated into the following (simplified) /GHC Core/ language
--
-- > w16_to_i32 = \x -> Just (case x of _ { W16# x# -> I32# (word2Int# x#) })
-- >
-- > i16_to_w16 = \x -> case eta of _
-- > { I16# b1 -> case tagToEnum# (<=# 0 b1) of _
-- > { False -> Nothing
-- > ; True -> Just (W16# (narrow16Word# (int2Word# b1)))
-- > }
-- > }
intCastMaybe :: (Integral a, Integral b, Bits a, Bits b) => a -> Maybe b
-- the code below relies on GHC optimizing away statically decidable branches
intCastMaybe x
| maybe True (<= x) yMinBound
, maybe True (x <=) yMaxBound = Just y
| otherwise = Nothing
where
y = fromIntegral x

xWidth = bitSizeMaybe x
yWidth = bitSizeMaybe y

yMinBound | isBitSubType x y = Nothing
| isSigned x, not (isSigned y) = Just 0
| isSigned x, isSigned y, Just yW <- yWidth
= Just (negate $ bit (yW-1)) -- N.B. assumes sub-type
| otherwise = Nothing

yMaxBound | isBitSubType x y = Nothing
| isSigned x, not (isSigned y), Just xW <- xWidth, Just yW <- yWidth
, xW <= yW+1 = Nothing -- max-bound beyond a's domain
| Just yW <- yWidth = if isSigned y then Just (bit (yW-1)-1) else Just (bit yW-1)
| otherwise = Nothing
{-# INLINEABLE intCastMaybe #-}
30 changes: 30 additions & 0 deletions LICENSE
Original file line number Diff line number Diff line change
@@ -0,0 +1,30 @@
Copyright (c) 2014, Herbert Valerio Riedel

All rights reserved.

Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are met:

* Redistributions of source code must retain the above copyright
notice, this list of conditions and the following disclaimer.

* Redistributions in binary form must reproduce the above
copyright notice, this list of conditions and the following
disclaimer in the documentation and/or other materials provided
with the distribution.

* Neither the name of Herbert Valerio Riedel nor the names of other
contributors may be used to endorse or promote products derived
from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
2 changes: 2 additions & 0 deletions Setup.hs
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
import Distribution.Simple
main = defaultMain
42 changes: 42 additions & 0 deletions int-cast.cabal
Original file line number Diff line number Diff line change
@@ -0,0 +1,42 @@
name: int-cast
version: 0.1.0.0
synopsis: Checked conversions between integral types
homepage: https://github.com/hvr/int-cast
bug-reports: https://github.com/hvr/int-cast/issues
license: BSD3
license-file: LICENSE
author: Herbert Valerio Riedel
maintainer: hvr@gnu.org
category: Data
build-type: Simple
cabal-version: >=1.10
description:
Provides statically or dynamically checked conversions between integral types.

source-repository head
type: git
location: https://github.com/hvr/int-cast.git

source-repository this
type: git
location: https://github.com/hvr/int-cast.git
tag: 0.1.0.0

library
default-language: Haskell2010
other-extensions:
CPP
DataKinds
TypeFamilies
TypeOperators
UndecidableInstances
build-depends: base ==4.7.*
exposed-modules: Data.IntCast

test-suite int-cast-test
default-language: Haskell2010
type: exitcode-stdio-1.0
hs-source-dirs: test .
main-is: Suite.hs
ghc-options: -Wall
build-depends: int-cast, base, test-framework ==0.8.*, test-framework-quickcheck2 ==0.3.*
Loading

0 comments on commit d1f8e84

Please sign in to comment.