Skip to content

Instantly share code, notes, and snippets.

@goldfirere
Last active December 25, 2015 02:29
Show Gist options
  • Save goldfirere/6902431 to your computer and use it in GitHub Desktop.
Save goldfirere/6902431 to your computer and use it in GitHub Desktop.
Strongly-typed version of code from GHC Trac #8423.
{-# LANGUAGE DataKinds, PolyKinds, GADTs, TypeFamilies, TypeOperators,
ConstraintKinds, ScopedTypeVariables, RankNTypes #-}
module Shape where
import GHC.Exts
data a :=: b where
Refl :: a :=: a
data Proxy a = Proxy
data Nat = Zero | Succ Nat
type family (n1 :: Nat) + (n2 :: Nat) :: Nat
type instance Zero + n2 = n2
type instance (Succ n1') + n2 = Succ (n1' + n2)
-- singleton for Nat
data SNat :: Nat -> * where
SZero :: SNat Zero
SSucc :: SNat n -> SNat (Succ n)
gcoerce :: (a :=: b) -> ((a ~ b) => r) -> r
gcoerce Refl x = x
-- inductive proof of right-identity of +
plus_id_r :: SNat n -> ((n + Zero) :=: n)
plus_id_r SZero = Refl
plus_id_r (SSucc n) = gcoerce (plus_id_r n) Refl
-- inductive proof of simplification on the rhs of +
plus_succ_r :: SNat n1 -> Proxy n2 -> ((n1 + (Succ n2)) :=: (Succ (n1 + n2)))
plus_succ_r SZero _ = Refl
plus_succ_r (SSucc n1) proxy_n2 = gcoerce (plus_succ_r n1 proxy_n2) Refl
data Shape :: Nat -> * where
Nil :: Shape Zero
(:*) :: Int -> Shape n -> Shape (Succ n)
reverseShape :: Shape n -> Shape n
reverseShape Nil = Nil
reverseShape list = go SZero Nil list
where
go :: SNat n1 -> Shape n1 -> Shape n2 -> Shape (n1 + n2)
go snat acc Nil = gcoerce (plus_id_r snat) acc
go snat acc (h :* (t :: Shape n3)) =
gcoerce (plus_succ_r snat (Proxy :: Proxy n3))
(go (SSucc snat) (h :* acc) t)
{-# LANGUAGE DataKinds, PolyKinds, GADTs, TypeFamilies, TypeOperators,
ConstraintKinds, ScopedTypeVariables, RankNTypes #-}
module Shape where
import GHC.Exts
import Data.Proxy
import Data.Type.Equality
data Nat = Zero | Succ Nat
type family n1 + n2 where
Zero + n2 = n2
(Succ n1') + n2 = Succ (n1' + n2)
-- singleton for Nat
data SNat :: Nat -> * where
SZero :: SNat Zero
SSucc :: SNat n -> SNat (Succ n)
gcoerce :: (a :=: b) -> ((a ~ b) => r) -> r
gcoerce Refl x = x
-- inductive proof of right-identity of +
plus_id_r :: SNat n -> ((n + Zero) :=: n)
plus_id_r SZero = Refl
plus_id_r (SSucc n) = gcoerce (plus_id_r n) Refl
-- inductive proof of simplification on the rhs of +
plus_succ_r :: SNat n1 -> Proxy n2 -> ((n1 + (Succ n2)) :=: (Succ (n1 + n2)))
plus_succ_r SZero _ = Refl
plus_succ_r (SSucc n1) proxy_n2 = gcoerce (plus_succ_r n1 proxy_n2) Refl
data Shape :: Nat -> * where
Nil :: Shape Zero
(:*) :: Int -> Shape n -> Shape (Succ n)
reverseShape :: Shape n -> Shape n
reverseShape Nil = Nil
reverseShape list = go SZero Nil list
where
go :: SNat n1 -> Shape n1 -> Shape n2 -> Shape (n1 + n2)
go snat acc Nil = gcoerce (plus_id_r snat) acc
go snat acc (h :* (t :: Shape n3)) =
gcoerce (plus_succ_r snat (Proxy :: Proxy n3))
(go (SSucc snat) (h :* acc) t)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment