Browse Source

Fix Adversarial.

tags/0.1.0.0
Thomas Kerber 1 year ago
parent
commit
8d75718e97
Signed by: Thomas Kerber <t.kerber@ed.ac.uk> GPG Key ID: 8489B911F9ED617B
4 changed files with 106 additions and 30 deletions
  1. +68
    -24
      src/Yggdrasil/Adversarial.hs
  2. +1
    -1
      src/Yggdrasil/ExecutionModel.hs
  3. +36
    -4
      src/Yggdrasil/HList.hs
  4. +1
    -1
      yggdrasil.cabal

+ 68
- 24
src/Yggdrasil/Adversarial.hs View File

@@ -1,39 +1,79 @@
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators #-}

module Yggdrasil.Adversarial
( WithAdversary
, Adversary
( Adversary
, WithAdversary
, NoAdversary(noAdversary)
, DummyInterfaces
, DummyAdversary(dummyAdversary)
, createAdversarial
, noAdversary
, dummyAdversary
) where

import Data.Dynamic (Typeable)
import Yggdrasil.ExecutionModel (Action,
Functionality (Functionality),
create, interface')
import Control.Monad.Trans.Class (lift)
import Yggdrasil.ExecutionModel (Action (Create),
Functionality (Functionality),
InterfaceMap, Interfaces, Operation,
Operations, Ref)
import Yggdrasil.HList (type (+|+), HList ((:::), Nil),
HSplit (hsplit))

type WithAdversary b c = Action (Maybe b) -> c
type family MaybeMap (bs :: [(*, *)]) = (ys :: [(*, *)]) | ys -> bs where
MaybeMap '[] = '[]
MaybeMap ('( a, b) ': xs) = '( a, Maybe b) ': MaybeMap xs

type Adversary s a b = Functionality s (Action (Maybe a), b)
type WithAdversary s (ts :: [(*, *)]) b
= HList (Interfaces s (MaybeMap ts)) -> b

noAdversary :: Adversary () a ()
noAdversary =
Functionality () ((, ()) <$> interface' (\_ -> return ((), Nothing)))
type Adversary s c as bs = Functionality s c (as +|+ MaybeMap bs)

dummyAdversary :: Action (Maybe b) -> Adversary () b ()
dummyAdversary ref = Functionality () (return (ref, ()))
class NoAdversary s (bs :: [(*, *)]) where
nullOperations :: HList (Operations s () (MaybeMap bs))
noAdversary :: Adversary s () '[] bs
noAdversary = Functionality () (nullOperations @s @bs)

instance NoAdversary s '[] where
nullOperations = Nil

instance NoAdversary s xs => NoAdversary s ('( a, b) ': xs) where
nullOperations = (\_ _ -> return Nothing) ::: nullOperations @s @xs

type family DummyInterfaces s (xs :: [(*, *)]) = (ys :: [*]) | ys -> xs where
DummyInterfaces s '[] = '[]
DummyInterfaces s ('( a, b) ': xs) = (Ref s -> a -> Action s b) ': DummyInterfaces s xs

class DummyAdversary s (bs :: [(*, *)]) where
operations ::
HList (DummyInterfaces s (MaybeMap bs))
-> HList (Operations s () (MaybeMap bs))
dummyAdversary ::
HList (DummyInterfaces s (MaybeMap bs)) -> Adversary s () '[] bs
dummyAdversary = Functionality () . operations @s @bs

instance DummyAdversary s '[] where
operations _ = Nil

instance DummyAdversary s bs => DummyAdversary s ('( a, b) ': bs) where
operations (b ::: bs) =
((\ref x -> lift $ b ref x) :: Operation s () a (Maybe b)) :::
operations @s @bs bs

createAdversarial ::
(Typeable s, Typeable s')
=> Adversary s a c
-> WithAdversary a (Functionality s' b)
-> Action (b, c)
createAdversarial adv fnc = do
(advFnc, advEnv) <- create adv
fncEnv <- create $ fnc advFnc
return (fncEnv, advEnv)
( HSplit (Interfaces s (as +|+ MaybeMap bs)) (Interfaces s as) (Interfaces s (MaybeMap bs))
, InterfaceMap s c (as +|+ MaybeMap bs)
)
=> Adversary s c as bs
-> WithAdversary s bs b
-> Action s (HList (Interfaces s as), b)
createAdversarial adv f = (\(a, b) -> (a, f b)) <$> hsplit <$> Create adv

+ 1
- 1
src/Yggdrasil/ExecutionModel.hs View File

@@ -37,7 +37,7 @@ import Yggdrasil.HList (HList ((:::), Nil))

type Operation s c a b = Ref s -> a -> StateT c (Action s) b

type family Operations s c (xs :: [(*, *)]) :: [*] where
type family Operations s c (xs :: [(*, *)]) = (ys :: [*]) | ys -> xs where
Operations s c '[] = '[]
Operations s c ('( a, b) ': xs) = Operation s c a b ': Operations s c xs


+ 36
- 4
src/Yggdrasil/HList.hs View File

@@ -1,12 +1,44 @@
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

module Yggdrasil.HList
( HList(..)
, type (+|+)
, HAppend((+++))
, HSplit(hsplit)
) where

data HList :: [*] -> * where
Nil :: HList '[]
(:::) :: a -> HList as -> HList (a ': as)

type family (as :: [k]) +|+ (bs :: [k]) :: [k] where
'[] +|+ bs = bs
(a ': as) +|+ bs = a ': (as +|+ bs)

class HAppend as bs where
(+++) :: HList as -> HList bs -> HList (as +|+ bs)

instance HAppend '[] bs where
_ +++ bs = bs

instance HAppend as bs => HAppend (a ': as) bs where
(a ::: as) +++ bs = a ::: (as +++ bs)

class HSplit hs as bs where
hsplit :: HList hs -> (HList as, HList bs)

instance HSplit bs '[] bs where
hsplit bs = (Nil, bs)

instance HSplit hs as bs => HSplit (a ': hs) (a ': as) bs where
hsplit (h ::: hs) = let (as, bs) = hsplit @hs @as @bs hs in (h ::: as, bs)

+ 1
- 1
yggdrasil.cabal View File

@@ -17,7 +17,7 @@ library
Yggdrasil.Distribution
Yggdrasil.ExecutionModel
Yggdrasil.Functionalities
-- Yggdrasil.Adversarial
Yggdrasil.Adversarial
Yggdrasil.HList
other-extensions: GADTs
Rank2Types

Loading…
Cancel
Save