Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
sample of making and using proofs with CmpNat (and unsafeCoerce)
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE UndecidableInstances #-}
import Data.Constraint ((:-)(Sub), Dict(Dict))
import Data.Kind (Type)
import Data.Singletons (sing)
import Data.Singletons.Prelude (Sing(SEQ, SFalse, SGT, SLT, STrue), (%+), (%-), (%>), sCompare)
import Data.Singletons.Prelude.Num (PNum((+), (-)))
import Data.Singletons.Prelude.Ord (POrd((>)))
import Data.Singletons.TypeLits (SNat, Sing(SNat))
import Data.Type.Equality
import GHC.TypeLits (CmpNat, KnownNat, Nat)
import Unsafe.Coerce (unsafeCoerce)
data Foo where
Foo
:: forall (index :: Nat) (len :: Nat).
(CmpNat index len ~ 'LT)
=> SNat index
-> SNat len
-> Foo
createFoo :: Foo
createFoo = Foo (sing @Nat @0) (sing @Nat @1)
incrementLength :: Foo -> Foo
incrementLength (Foo index len) =
case bar index len of
Sub Dict -> Foo index (len %+ (sing @_ @1))
bar :: forall n m. Sing n -> Sing m -> (CmpNat n m ~ 'LT) :- (CmpNat n (m + 1) ~ 'LT)
bar SNat SNat = Sub axiom
where
axiom :: CmpNat n m ~ 'LT => Dict (CmpNat n (m + 1) ~ 'LT)
axiom = unsafeCoerce (Dict :: Dict (a ~ a))
-------------------------------------------------
data Bar :: Nat -> Nat -> Type where
Bar
:: forall (index :: Nat) (len :: Nat).
(KnownNat index, KnownNat len, CmpNat index len ~ 'LT)
=> Bar index len
data Foo2 where
Foo2 :: Bar index len -> Foo2
createFoo2 :: Foo2
createFoo2 = Foo2 $ Bar @0 @1
incrementLength2 :: Foo2 -> Foo2
incrementLength2 (Foo2 b) = Foo2 $ incLen b
incLen :: forall n m. Bar n m -> Bar n (m + 1)
incLen Bar =
case bar (sing @_ @n) (sing @_ @m) of
Sub Dict ->
case (sing @_ @m) %+ (sing @_ @1) of
SNat -> Bar
decrementLength2 :: Foo2 -> Maybe Foo2
decrementLength2 (Foo2 b) =
case decLen2 b of
Nothing -> Nothing
Just newB -> Just $ Foo2 newB
decLen :: forall n m. (CmpNat n (m - 1) ~ 'LT) => Bar n m -> Bar n (m - 1)
decLen Bar =
case (sing @_ @m) %- (sing @_ @1) of
SNat -> Bar
decLen2 :: forall n m. Bar n m -> Maybe (Bar n (m - 1))
decLen2 Bar =
case sCompare (sing @_ @n) ((sing @_ @m) %- (sing @_ @1)) of
SLT ->
case sing @_ @m %> sing @_ @0 of
STrue ->
case law2 (sing @_ @m) of
Sub Dict -> Just Bar
SFalse -> Nothing
SEQ -> Nothing
SGT -> Nothing
-- XXX: BEWARE! The following is incorrect.
-- For the reason why, see here:
-- https://stackoverflow.com/a/49710029/3040129
law2 :: forall m. Sing m -> (KnownNat m, m > 0 ~ 'True) :- KnownNat (m - 1)
law2 SNat = Sub axiom
where
axiom :: (KnownNat m, m > 0 ~ 'True) => Dict (KnownNat (m - 1))
axiom = unsafeCoerce (Dict :: forall a. Dict (a ~ 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