Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
negative information flow?
{-# language LambdaCase #-}
{-# language BlockArguments #-}
{-# language DataKinds #-}
{-# language PolyKinds #-}
{-# language LinearTypes #-}
{-# language StandaloneKindSignatures #-}
{-# language TypeOperators #-}
{-# language KindSignatures #-}
{-# language RankNTypes #-}
{-# language EmptyCase #-}
{-# language GADTs #-}
{-# language TypeFamilies #-}
{-# language UndecidableInstances #-}
{-# options_ghc -Wall #-}
module N where
import Data.Kind
import Linear.Logic
import Linear.Logic.Internal
data Rec (xs :: [i]) (f :: i -> Type) where
Nil :: Rec '[] f
Cons :: f a %1 -> Rec as f %1 -> Rec (a ': as) f
-- heyting negation
newtype NotRec (xs :: [i]) (f :: i -> Type) =
NotRec { runNotRec :: forall r. Rec xs f %1 -> r }
data Ix (xs :: [i]) (x :: i) where
H :: Ix (a ': as) a
T :: Ix as a -> Ix (b ': as) a
-- heyting negation
newtype NotIx (xs :: [i]) (x :: i) =
NotIx { runNotIx :: forall r. Ix xs x %1 -> r }
instance Prop' (Rec n f) where
type Not (Rec n f) = NotRec n f
r != NotRec f = f r
instance Prop' (NotRec n f) where
type Not (NotRec n f) = Rec n f
NotRec f != r = f r
instance Prop' (Ix as a) where
type Not (Ix as a) = NotIx as a
r != NotIx f = f r
instance Prop' (NotIx as a) where
type Not (NotIx as a) = Ix as a
x != y = y != x
type Name = String
data Term (as :: [Type]) (a :: Type) where
Var :: Ix as a %1 -> Term as a
App :: Term as (a -> b) %1 -> Term as a %1 -> Term as b
Lam :: Name -> Term (a ': as) b %1 -> Term as (a -> b)
newtype NotTerm (as :: [Type]) (a :: Type) =
NotTerm { runNotTerm :: forall r. Term as a %1 -> r }
instance Prop' (Term as a) where
type Not (Term as a) = NotTerm as a
tm != NotTerm f = f tm
instance Prop' (NotTerm as a) where
type Not (NotTerm as a) = Term as a
NotTerm f != tm = f tm
data Val a where
VLam :: Env as %1 -> Name %1 -> Term (a ': as) b %1 -> Val (a -> b)
VLit :: a -> Val a
newtype NotVal a = NotVal { runNotVal :: forall r. Val a %1 -> r }
instance Prop' (Val a) where
type Not (Val a) = NotVal a
tm != NotVal f = f tm
instance Prop' (NotVal a) where
type Not (NotVal a) = Val a
NotVal f != tm = f tm
type Env as = Rec as Val
($$) :: (Prop' a, Prop' b) => a b %1 -> a -> b
f $$ a = runImp f R a
infixl 0 $$
index :: Ix as a Rec as Val Val a
index = imp \case
L -> \(Noimp vna na) -> whyNot \n -> (index $$ n $$ vna) != na
R -> \f -> imp \case
L -> \na -> whyNot \case
Nil -> (case f of) na
Cons a as -> case f of
H -> a != na
T n -> (index $$ n $$ as) != na
R -> \(Cons a as) -> case f of
H -> a
T n -> index $$ n $$ as
eval :: Env as Term as a Val a
eval = imp \case
L -> \(Noimp t nv) -> whyNot \e -> (eval $$ e $$ t) != nv
R -> \e -> imp \case
L -> \nv -> whyNot \t -> (eval $$ e $$ t) != nv
R -> \case
Var n -> index $$ n $$ e
App f x -> apply $$ (eval $$ e $$ f) $$ (eval $$ e $$ x)
Lam n b -> VLam e n b
apply :: Val (a -> b) Val a Val b
apply = imp \case
R -> \case
VLam e _ b -> imp \case
R -> \v -> eval $$ Cons v e $$ b
L -> \nv -> whyNot \v -> (eval $$ Cons v e $$ b) != nv
VLit f -> imp \case
R -> \v -> VLit (f (run' v))
L -> \nvb -> whyNot \va -> VLit (f (run' va)) != nvb
L -> \(Noimp v nv) -> whyNot \u -> (apply $$ u $$ v) != nv
run' :: Val a -> a
run' (VLam e _ b) = \x -> run' (eval $$ Cons (VLit x) e $$ b)
run' (VLit x) = x
run :: Val a a
run = imp \case
L -> \na -> whyNot \va -> run' va != na
R -> run'
id_ :: Val (a -> a)
id_ = eval $$ Nil $$ Lam "x" (Var H)
const_ :: Val (a -> b -> a)
const_ = eval $$ Nil $$ (Lam "x" $ Lam "y" $ Var (T H))
kid :: Val (a -> b -> b)
kid = eval $$ Cons id_ (Cons const_ Nil) $$ App (Var (T H)) (Var H)
devoid:: NotVal Void
devoid = NotVal \case
VLit x -> case x of
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment