Skip to content

Instantly share code, notes, and snippets.

@cdparks

cdparks/Add.hs

Last active Jun 11, 2020
Embed
What would you like to do?
Luv 2 type addition
-- An unserious response to
--
-- > I will believe in type systems the day one of them warns me about this code:
-- > pub fn add_two_integers(num1: Int, num2: Int) -> Int {
-- > num1 - num2
-- > }
--
-- I don't understand why people don't want to program like this. Types!
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
import Data.Proxy (Proxy(..))
import GHC.TypeLits (type (+), type (-), KnownNat(..))
import qualified GHC.TypeLits as TypeLits
-- | Kind of natural numbers
data Nat = Z | S Nat deriving (Eq, Ord, Show)
-- | Type-level addition on natural numbers
type family Add (n :: Nat) (m :: Nat) :: Nat where
Add 'Z m = m
Add ('S n) m = 'S (Add n m)
-- | Term-level natural numbers indexed by their type
--
-- "Singleton" natural numbers.
--
data SNat (n :: Nat) where
SZ :: SNat 'Z
SS :: SNat n -> SNat ('S n)
deriving instance Show (SNat n)
-- | "Typed" Term level addition of natural numbers
add :: SNat n -> SNat m -> SNat (Add n m)
add SZ m = m
add (SS n) m = SS (add n m)
-- | Convert GHC type literals to our '@Nat'@ kind
type family FromLit (t :: TypeLits.Nat) :: Nat where
FromLit 0 = 'Z
FromLit n = 'S (FromLit (n - 1))
-- | Typeclass for converting GHC type literals to term level natural numbers
class Lit (t :: TypeLits.Nat) (n :: Nat) where
litProxy :: p t -> SNat n
-- | Base case: we can always convert '0' to 'Z'
instance Lit 0 'Z where
litProxy _ = SZ
-- | Inductive case: apply 'SS' to 'litProxy (Proxy @(t - 1))'
instance (KnownNat t, FromLit t ~ n, n ~ 'S m, u ~ (t - 1), Lit u m) => Lit t ('S m) where
litProxy _ = SS (litProxy (Proxy @u))
-- | Non-proxy version of 'litProxy'. Use a type application
lit :: forall t n . (KnownNat t, n ~ FromLit t, Lit t n) => SNat n
lit = litProxy (Proxy @t)
-- | Beware! Type erasure!
toInt :: SNat n -> Int
toInt SZ = 0
toInt (SS n) = 1 + toInt n
-- | Typed addition!
main :: IO ()
main = print $ toInt n
where
n :: SNat (Add (FromLit 4) (FromLit 5))
n = add (lit @4) (lit @5)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.