public
Last active

Strongly-typed version of code from GHC Trac #8423.

  • Download Gist
Shape-7.6.hs
Haskell
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50
{-# 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)
Shape.hs
Haskell
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47
{-# 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)

Please sign in to comment on this gist.

Something went wrong with that request. Please try again.