Giving Int a Promotion

Lies.hs

{-# Language RankNTypes #-}
{-# Language PolyKinds #-}
{-# Language DataKinds #-}
{-# Language PatternSynonyms #-}
{-# Language ViewPatterns #-}
{-# Language RoleAnnotations #-}
{-# Language StandaloneKindSignatures #-}
{-# Language TypeFamilies #-}
{-# Language TypeOperators #-}
{-# Language GADTs #-}
{-# Language FlexibleInstances #-}
{-# Language TypeApplications #-}
{-# Language AllowAmbiguousTypes #-}
{-# Language ScopedTypeVariables #-}

module Lies where

import Data.Proxy
import Data.Kind
import Data.Type.Equality
import GHC.TypeNats
import Unsafe.Coerce

type Z = 0
type S n = 1+n

--------------------------------------------------------------------------------
-- * Singletons
--------------------------------------------------------------------------------

class SingKind k where
  type Sing :: k -> Type
  fromSing :: Sing (a :: k) -> k

class SingI (a :: k) where
  sing :: Sing a

--------------------------------------------------------------------------------
-- * Lifting Ints
--------------------------------------------------------------------------------

type MAX_WORD = 18446744073709551615 -- todo: detect architecture, etc.
type MOD_WORD = 18446744073709551616

data family MkInt' :: Nat -> k
type MkInt :: Nat -> Int
type MkInt = MkInt'

type SInt :: Int -> Type
type role SInt nominal
newtype SInt n = UnsafeSInt { sintVal :: Int } deriving Show

instance SingKind Int where
  type Sing = SInt
  fromSing (UnsafeSInt n) = n

instance (KnownNat n, n <= MAX_WORD) => SingI (MkInt n) where
  sing = UnsafeSInt $ fromIntegral @_ @Int $ fromIntegral @_ @Word $ natVal $ Proxy @n

-- this instance is what really requires the side condition that the n is <= maxBound @Word
-- arguably we should finish hiding MkInt' and make MkInt compute the modulus to enforce this
-- invariant
instance TestEquality SInt where
  testEquality (UnsafeSInt i) (UnsafeSInt j) 
    | i == j    = Just (unsafeCoerce Refl)
    | otherwise = Nothing

--------------------------------------------------------------------------------
-- * Emulating a GADT
--------------------------------------------------------------------------------

data SInt' (n :: Int) where
  SIZ' :: SInt' (MkInt Z)
  SIS' :: SInt (MkInt i) -> SInt' (MkInt (S i `Mod` MOD_WORD))

upSInt :: SInt n -> SInt' n
upSInt (UnsafeSInt 0) = unsafeCoerce SIZ'
upSInt (UnsafeSInt n) = unsafeCoerce (SIS' (UnsafeSInt (n-1)))

pattern SIZ :: () => (n ~ MkInt Z) => SInt n
pattern SIZ <- (upSInt -> SIZ') where
  SIZ = UnsafeSInt 0

pattern SIS :: () => (i ~ MkInt i', j ~ MkInt (S i' `Mod` MOD_WORD)) => SInt i -> SInt j
pattern SIS n <- (upSInt -> SIS' n) where
  SIS n = UnsafeSInt (1 + sintVal n)

{-# complete SIZ, SIS #-}

LiesWithSucc.hs

{-# Language RankNTypes #-}
{-# Language PolyKinds #-}
{-# Language DataKinds #-}
{-# Language PatternSynonyms #-}
{-# Language DerivingStrategies #-}
{-# Language GeneralizedNewtypeDeriving #-}
{-# Language ViewPatterns #-}
{-# Language RoleAnnotations #-}
{-# Language StandaloneKindSignatures #-}
{-# Language TypeFamilies #-}
{-# Language TypeOperators #-}
{-# Language GADTs #-}
{-# Language FlexibleInstances #-}
{-# Language TypeApplications #-}
{-# Language AllowAmbiguousTypes #-}
{-# Language ScopedTypeVariables #-}

module Lies where

import Control.Exception
import Data.Proxy
import Data.Kind
import Data.Type.Equality
import GHC.TypeNats
import Numeric.Natural
import Unsafe.Coerce

type Z = 0
type S n = 1+n

--------------------------------------------------------------------------------
-- * Singletons
--------------------------------------------------------------------------------

class SingKind k where
  type Sing :: k -> Type
  fromSing :: Sing (a :: k) -> k

class SingI (a :: k) where
  sing :: Sing a

--------------------------------------------------------------------------------
-- * Lifting Ints
--------------------------------------------------------------------------------

data family MkInt' :: Nat -> k
type MkInt :: Nat -> Int
type MkInt = MkInt'

type SInt :: Int -> Type
type role SInt nominal
newtype SInt n = UnsafeSInt { sintVal :: Int }
  deriving newtype Show

instance SingKind Int where
  type Sing = SInt
  fromSing (UnsafeSInt n) = n

instance KnownNat n => SingI (MkInt n) where
  sing 
    | n > fromIntegral (maxBound @Word) = throw Overflow
    | otherwise = UnsafeSInt (fromIntegral n)
    where n = natVal $ Proxy @n

instance TestEquality SInt where
  testEquality (UnsafeSInt i) (UnsafeSInt j) 
    | i == j    = Just (unsafeCoerce Refl)
    | otherwise = Nothing

--------------------------------------------------------------------------------
-- * Emulating a GADT
--------------------------------------------------------------------------------

data SInt' (n :: Int) where
  SIZ' :: SInt' (MkInt Z)
  SIS' :: SInt (MkInt i) -> SInt' (MkInt (S i))

upSInt :: SInt n -> SInt' n
upSInt (UnsafeSInt 0) = unsafeCoerce SIZ'
upSInt (UnsafeSInt n) = unsafeCoerce (SIS' (UnsafeSInt (n-1)))

pattern SIZ :: () => (n ~ MkInt Z) => SInt n
pattern SIZ <- (upSInt -> SIZ') where
  SIZ = UnsafeSInt 0

pattern SIS :: () => (i ~ MkInt i', j ~ MkInt (S i')) => SInt i -> SInt j
pattern SIS n <- (upSInt -> SIS' n) where
  SIS n = UnsafeSInt (succ $ sintVal n)

{-# complete SIZ, SIS #-}

Arguably I should streamline SIS, and make it fail during construction if the data type is maxBound by using succ. Then I could strip a bunch of MOD_WORD stuff because testEquality would bomb due to the presence of the error.

https://gist.github.com/ekmett/0e5378b47a1248fc0059078d6a649d55 is much more comprehensive, if less focused than these versions.

https://github.com/ekmett/haskell/tree/master/types subsumes this.