aj/purescript-singletons
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Newtype some more to get reify working

Browse source
This commit is contained in:
Anupam Jain 2024-10-22 14:29:56 +05:30
parent 08c9f02f31
commit d95a4f0983
1 changed files with 14 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

25
src/Singletons.purs
View file

@ -2,7 +2,7 @@ module Singletons where
import Control.Category (identity, (<<<))
import Data.Exists (Exists, mkExists, runExists)
import Data.Function (flip, (#))
import Data.Function ((#))
import Data.Leibniz (type (~), runLeibniz, symm)
data Nat
@ -32,9 +32,8 @@ reflect' = case _ of
SSucc p -> p # runExists \ (Prev s _) -> Succ (reflect' s)
-- Term -> Type
-- Why DOES this NOT work
-- reify :: forall r. (forall p. SNatOf p => r) -> Nat -> r
-- reify x n = runExists (withDNat x) (toSomeNat n)
reify :: forall r. (forall p. Res p r) -> Nat -> r
reify x n = runExists (withDNat x) (toSomeNat n)
-- Isomorphic to Nat
type SomeNat = Exists SNat
@ -50,21 +49,25 @@ toSomeNat (Succ n) = toSomeNat n # runExists \sn -> mkExists (SSucc (mkExists (P
ssucc :: SomeNat -> SomeNat
ssucc = toSomeNat <<< Succ <<< fromSomeNat
newtype DNat p = DNat (forall r. (SNatOf p => r) -> r)
-- This is a newtype because - In a definition like this - `provideDNat x (DNat f) = f x`, where `f :: SNatOf p => r`
-- the PS typchecker sees `f x` and elaborates `x` to take the `SNatOf` constraint even though it may not need it
-- If we block off the constraint inside a newtype, it doesn't do this
newtype Res p r = Res (SNatOf p => r)
-- This is a newtype because runLeibniz needs it to be of the form `TypConstr p``
-- And it doesn't seem to work well with type aliases
newtype DNat p = DNat (forall r. Res p r -> r)
captureDNat :: forall @p. SNatOf p => DNat p
captureDNat = DNat \r -> r
captureDNat = DNat \ (Res r) -> r
provideDNat :: forall p r. (SNatOf p => r) -> DNat p -> r
provideDNat = flip unDNat
unDNat :: forall p r. DNat p -> (SNatOf p => r) -> r
unDNat :: forall p r. DNat p -> Res p r -> r
unDNat (DNat f) = f
dNat :: forall p. SNat p -> DNat p
dNat s = DNat (\x -> withDNat x s)
withDNat :: forall p r. (SNatOf p => r) -> SNat p -> r
withDNat :: forall p r. Res p r -> SNat p -> r
withDNat x sn = case sn of
SZero w -> unDNat (runLeibniz (symm w) (captureDNat @PZero)) x
SSucc e -> e # runExists \ (Prev _ w) -> unDNat (runLeibniz (symm w) (dNat (runLeibniz w sn))) x