Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Using a structural type (type level Peano numbers) to try to simplify the replicateVec function.
{-# 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 VectStuff3 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((+), (-)), SNum((%-)), SingI, SingKind(Demote, fromSing, toSing),
SomeSing(SomeSing), sing, withSomeSing)
import Data.Singletons.TypeLits (KnownNat, Nat, SNat, Sing(SNat), natVal)
-- import GHC.TypeLits (Nat {-CmpNat, KnownNat, Nat, natVal-})
import GHC.Natural (Natural)
import Unsafe.Coerce (unsafeCoerce)
newtype MyNat = MyNatCon Nat
data instance Sing (z :: MyNat) where
SZ :: Sing ('MyNatCon 0)
SSucc :: KnownNat n => Sing ('MyNatCon n) -> Sing ('MyNatCon (1 + n))
deriving instance Show (Sing (z :: MyNat))
axiom :: Dict (a ~ b)
axiom = unsafeCoerce (Dict :: Dict (a ~ a))
plusMinusNM :: forall n m. Dict ((m + (n - m)) ~ n)
plusMinusNM = axiom
nMinus1isSNatProof :: forall n. Refuted (n :~: 0) -> SNat n -> SNat (n - 1)
nMinus1isSNatProof _ SNat = (sing @_ @n) %- (sing @_ @1)
singNatToMyNatCon :: forall n. Sing n -> Sing ('MyNatCon n)
singNatToMyNatCon snat =
case snat %~ (sing @_ @0) of
Proved Refl -> SZ
Disproved f ->
case plusMinusNM @n @1 of
Dict ->
case nMinus1isSNatProof f snat of
snat'@SNat -> SSucc (singNatToMyNatCon snat')
mPlus1IsKnownNat :: forall n m o. ('MyNatCon n ~ 'MyNatCon (o + m), KnownNat m, KnownNat o) :- KnownNat n
mPlus1IsKnownNat =
Sub $
let int = natVal (Proxy @m) + natVal (Proxy @o)
in
case toSing int of
SomeSing (SNat :: Sing x) ->
unsafeCoerce (Dict :: Dict (KnownNat x)) int
myNatConToSingNat :: forall n. Sing ('MyNatCon n) -> Sing n
myNatConToSingNat SZ = sing @_ @0
myNatConToSingNat (SSucc (_ :: Sing ('MyNatCon m))) =
case mPlus1IsKnownNat @n @m @1 of
Sub Dict -> sing @_ @(1 + m)
instance SingI n => SingI ('MyNatCon n) where
sing :: Sing ('MyNatCon n)
sing = singNatToMyNatCon $ sing @_ @n
data Vect n a where
VNil :: Vect 0 a
VCons :: a -> Vect n a -> Vect (1 + n) a
newtype MyNatural = MyNatural Natural deriving (Num, Show)
instance SingKind MyNat where
type Demote MyNat = MyNatural
fromSing :: forall (a :: MyNat). Sing a -> MyNatural
fromSing SZ = MyNatural . fromSing $ myNatConToSingNat SZ -- fromSing . myNatConToSingNat
fromSing x@(SSucc _) = MyNatural . fromSing $ myNatConToSingNat x
toSing :: MyNatural -> SomeSing MyNat
toSing (MyNatural n) = withSomeSing n $ SomeSing . singNatToMyNatCon
replicateVec :: Sing ('MyNatCon n) -> a -> Vect n a
replicateVec SZ _ = VNil
replicateVec (SSucc s) a = VCons a $ replicateVec s 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

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