Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Writing replicateVec without needing the magic trick. A little simpler.
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeInType #-}
module VectStuff2 where
import Data.Constraint ((:-)(Sub), Dict(Dict))
import Data.Kind (Type)
import Data.Singletons.Decide (Decision(Disproved, Proved), Refuted, (:~:)(Refl), (%~))
import Data.Singletons.Prelude (PNum((-), (+)), SNum((%-)), sing)
import Data.Singletons.TypeLits (KnownNat, Nat, SNat, Sing(SNat), natVal)
-- import GHC.TypeLits (Nat {-CmpNat, KnownNat, Nat, natVal-})
import Unsafe.Coerce (unsafeCoerce)
data Vect :: Nat -> Type -> Type where
VNil :: Vect 0 a
VCons :: a -> Vect n a -> Vect (n + 1) a
deriving instance Show a => Show (Vect n a)
axiom :: Dict a
axiom = unsafeCoerce (Dict :: Dict (a ~ a))
plusMinusEqLaw :: forall n m. Dict (n ~ ((n - m) + m))
plusMinusEqLaw = axiom
nMinus1isSNatProof :: forall n. Refuted (n :~: 0) -> SNat n -> SNat (n - 1)
nMinus1isSNatProof _ SNat = (sing @_ @n) %- (sing @_ @1)
replicateVec :: forall n a. SNat n -> a -> Vect n a
replicateVec snat a =
case snat %~ (sing @_ @0) of
Proved Refl -> VNil
Disproved f ->
case nMinus1isSNatProof f snat of
snat'@SNat ->
case plusMinusEqLaw @n @1 of
Dict ->
VCons a $ replicateVec snat' a
@cdepillabout
Copy link
Author

cdepillabout commented Apr 8, 2018

This can be loaded into GHCI with the following command:

$ stack --resolver nightly-2018-03-18 ghci --package classy-prelude  --package singletons --package containers --package typelits-witnesses --package constraints

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment