Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Writing replicateVec without depending on the singleton library and without using structural typing.
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeInType #-}
module VectStuff4 where
import Data.Constraint (Dict(Dict))
import Data.Kind (Type)
import Data.Proxy (Proxy(Proxy))
import Data.Type.Equality
import GHC.TypeLits
(type (+), type (-), KnownNat, Nat, SomeNat(SomeNat),
natVal, sameNat, someNatVal)
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)
plusMinusEq :: forall n m. Dict (n ~ ((n - m) + m))
plusMinusEq = unsafeCoerce (Dict :: Dict ())
unsafeKnownNat :: forall n. KnownNat n => Dict (KnownNat (n - 1))
unsafeKnownNat =
let int = natVal (Proxy @n) - 1
in
case someNatVal int of
Nothing -> error "error"
Just (SomeNat (Proxy :: Proxy x)) ->
unsafeCoerce (Dict :: Dict (KnownNat x)) int
replicateVec :: forall n a. KnownNat n => a -> Vect n a
replicateVec a =
case sameNat (Proxy @n) (Proxy @0) of
Just Refl -> VNil
Nothing ->
case plusMinusEq @n @1 of
Dict ->
case unsafeKnownNat @n of
Dict -> VCons a $ replicateVec @(n - 1) a
@cdepillabout
Copy link
Author

cdepillabout commented Apr 8, 2018

@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

@Lysxia
Copy link

Lysxia commented Apr 9, 2018

I think unsafeCoerce (Dict :: Dict (KnownNat x)) int should be unsafeCoerce (Dict :: Dict (KnownNat x)), but I have no idea why it works even with that extra argument. It's probably a combination of very low level implementation details.

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