Created
April 13, 2021 03:37
Star
You must be signed in to star a gist
negative information flow?
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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