Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Using a magic trick to prove laws about replicateVec
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeInType #-}
module VectStuff where
import Data.Constraint ((:-)(Sub), Dict(Dict))
import Data.Kind (Type)
import Data.Proxy (Proxy(Proxy))
import Data.Singletons.Decide (Decision(Disproved, Proved), Refuted, (:~:)(Refl), (%~))
import Data.Singletons.Prelude (PNum((-)), sing)
import Data.Singletons.TypeLits (SNat, Sing(SNat))
import GHC.TypeLits (CmpNat, KnownNat, Nat, natVal)
import Unsafe.Coerce (unsafeCoerce)
data Vect :: Nat -> Type -> Type where
VNil :: Vect 0 a
VCons :: forall n a. CmpNat n 0 ~ 'GT => a -> Vect (n - 1) a -> Vect n a
deriving instance Show a => Show (Vect n a)
axiom :: Dict a
axiom = unsafeCoerce (Dict :: Dict (a ~ a))
newtype Magic n = Magic (KnownNat n => Dict (KnownNat n))
magic ::
forall n m o.
(Integer -> Integer -> Integer)
-> (KnownNat n, KnownNat m) :- KnownNat o
magic f =
Sub $ unsafeCoerce (Magic Dict) (natVal (Proxy @n) `f` natVal (Proxy @m))
nMinus1isSNatProof :: forall n. Refuted (n :~: 0) -> SNat n -> Dict (KnownNat (n - 1))
nMinus1isSNatProof _ SNat =
case magic @n @1 @(n - 1) (-) of
Sub d -> d
nGT0Proof :: forall n. Refuted (n :~: 0) -> SNat n -> SNat (n - 1)
nGT0Proof f sNat =
case nMinus1isSNatProof f sNat of
Dict -> SNat
snatMinus1NGT0Law :: forall n. SNat (n - 1) -> Dict (CmpNat n 0 ~ 'GT)
snatMinus1NGT0Law _ = axiom
replicateVec :: forall n a. SNat n -> a -> Vect n a
replicateVec snat a =
case snat %~ (sing @_ @0) of
Proved Refl -> VNil
Disproved f ->
case nGT0Proof f snat of
snat' ->
case snatMinus1NGT0Law snat' of
Dict ->
VCons a $ replicateVec snat' a
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment