Browse Source

Type level party management!

oldhaskell
Thomas Kerber 1 year ago
parent
commit
ce9a551408
Signed by: Thomas Kerber <t.kerber@ed.ac.uk> GPG Key ID: 8489B911F9ED617B
4 changed files with 185 additions and 44 deletions
  1. +34
    -12
      src/Yggdrasil/HList.hs
  2. +67
    -32
      src/Yggdrasil/MetaProtocol.hs
  3. +83
    -0
      src/Yggdrasil/Nat.hs
  4. +1
    -0
      yggdrasil.cabal

+ 34
- 12
src/Yggdrasil/HList.hs View File

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

-- | Provides heterogeneous lists through 'HList', as well as some type and
-- value level operations on them.
@@ -17,9 +18,12 @@ module Yggdrasil.HList
, type (+|+)
, HAppend((+++))
, HSplit(hsplit)
, HSequence(hsequence)
, Applied
) where

infixr 5 :::

-- | A heterogeneous list.
data HList :: [*] -> * where
Nil :: HList '[]
@@ -48,4 +52,22 @@ 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)
hsplit (h ::: hs) =
let (as, bs) = hsplit @hs @as @bs hs
in (h ::: as, bs)

type family Applied m (as :: [k]) = (ys :: [k]) | ys -> as where
Applied m '[] = '[]
Applied m (a ': as) = m a ': Applied m as

class HSequence m as where
hsequence :: HList (Applied m as) -> m (HList as)

instance Monad m => HSequence m '[] where
hsequence Nil = return Nil

instance (Monad m, HSequence m as) => HSequence m (a ': as) where
hsequence (a ::: as) = do
a' <- a
as' <- hsequence @m @as as
return (a' ::: as')

+ 67
- 32
src/Yggdrasil/MetaProtocol.hs View File

@@ -1,18 +1,20 @@
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators #-}

module Yggdrasil.MetaProtocol
( MetaProtocol
, Relay
, RelayN
, npartyIdeal
, npartyReal
) where
@@ -23,49 +25,82 @@ import Yggdrasil.ExecutionModel (Action (Create),
Functionality (Functionality),
InterfaceMap, Interfaces,
Operations)
import Yggdrasil.HList (HList ((:::), Nil))
import Yggdrasil.HList (HList ((:::), Nil),
HSequence (hsequence))
import Yggdrasil.Nat (ForEach, ForEach (foreach),
IdApplied (idApplied), NCopies, Zn)

type MetaProtocol s c c' ops ops'
= Functionality s c ops -> Functionality s c' ops'

class Relay s (ops :: [(*, *)]) where
operations :: (HList (Interfaces s ops)) -> (HList (Operations s () ops))
relay :: (HList (Interfaces s ops)) -> Functionality s () ops
relay is = Functionality () (operations @s @ops is)
class RelayN s n (ops :: [(*, *)]) where
relayNOperations ::
(HList (Interfaces s (WithZn n ops)))
-> Zn n
-> (HList (Operations s () ops))
relayN ::
(HList (Interfaces s (WithZn n ops))) -> Zn n -> Functionality s () ops
relayN is n = Functionality () (relayNOperations @s @n @ops is n)

instance Relay s '[] where
operations _ = Nil
instance RelayN s n '[] where
relayNOperations _ _ = Nil

instance Relay s xs => Relay s ('( a, b) ': xs) where
operations (f ::: xs) = lifted ::: operations @s @xs xs
instance RelayN s n xs => RelayN s n ('( a, b) ': xs) where
relayNOperations (f ::: xs) n = lifted ::: relayNOperations @s @n @xs xs n
where
lifted _ a = lift (f a)
lifted _ a = lift (f (n, a))

type family WithZn n (ops :: [(*, *)]) = (ys :: [(*, *)]) | ys -> ops where
WithZn n '[] = '[]
WithZn n ('( a, b) ': xs) = '( (Zn n, a), b) ': WithZn n xs

npartyIdeal ::
(InterfaceMap s c ops, InterfaceMap s () ops, Relay s ops)
=> Integer
-> MetaProtocol s c (Maybe [HList (Interfaces s ops)]) ops '[ '( (), [HList (Interfaces s ops)])]
npartyIdeal n f = Functionality Nothing (mkOp ::: Nil)
forall s c n ops.
( ForEach n (Action s (HList (Interfaces s ops)))
, IdApplied (Action s) n (HList (Interfaces s ops))
, RelayN s n ops
, InterfaceMap s c (WithZn n ops)
, InterfaceMap s () ops
, HSequence (Action s) (NCopies n (HList (Interfaces s ops)))
)
=> MetaProtocol s c
(Maybe (HList (NCopies n (HList (Interfaces s ops)))))
(WithZn n ops)
'[ '( (), HList (NCopies n (HList (Interfaces s ops))))]
npartyIdeal f = Functionality Nothing (mkOp ::: Nil)
where
mkOp _ _ =
get >>= \case
Just i -> return i
Nothing -> do
f0 <- lift $ Create f
is <- (lift . sequence) [Create (relay f0) | _ <- [1 .. n]]
is <-
(lift .
hsequence . idApplied @(Action s) @n @(HList (Interfaces s ops)))
(foreach (\i -> Create (relayN @s @n @ops f0 i)))
put (Just is)
return is

npartyReal ::
(InterfaceMap s c ops)
=> Integer
-> MetaProtocol s c (Maybe [HList (Interfaces s ops)]) ops '[ '( (), [HList (Interfaces s ops)])]
npartyReal n f = Functionality Nothing (mkOp ::: Nil)
forall s c n ops.
( ForEach n (Action s (HList (Interfaces s ops)))
, IdApplied (Action s) n (HList (Interfaces s ops))
, InterfaceMap s c ops
, HSequence (Action s) (NCopies n (HList (Interfaces s ops)))
)
=> MetaProtocol s c
(Maybe (HList (NCopies n (HList (Interfaces s ops)))))
ops
'[ '( (), HList (NCopies n (HList (Interfaces s ops))))]
npartyReal f = Functionality Nothing (mkOp ::: Nil)
where
mkOp _ _ =
get >>= \case
Just i -> return i
Nothing -> do
is <- (lift . sequence) [Create f | _ <- [1 .. n]]
is <-
(lift .
hsequence . idApplied @(Action s) @n @(HList (Interfaces s ops)))
(foreach (\_ -> Create f))
put (Just is)
return is

+ 83
- 0
src/Yggdrasil/Nat.hs View File

@@ -0,0 +1,83 @@
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Yggdrasil.Nat
( Nat
, Zero
, Succ
, NCopies
, Zn
, ForEach(foreach)
, IdApplied(idApplied)
, mkZn
, unZn
) where

import Data.Maybe (fromJust)
import Yggdrasil.HList (Applied, HList ((:::), Nil))

data Zero

data Succ n

class Nat n where
asInt :: Integral i => i

instance Nat Zero where
asInt = 0

instance Nat n => Nat (Succ n) where
asInt = asInt @n + 1

data Zn n =
Zn Integer
deriving (Eq, Show, Ord)

mkZn ::
forall n. Nat n
=> Integer
-> Maybe (Zn n)
mkZn x
| x < 0 = Nothing
| x > asInt @n = Nothing
| otherwise = Just (Zn x)

unZn :: Zn n -> Integer
unZn (Zn n) = n

promote :: Zn n -> Zn (Succ n)
promote (Zn n) = Zn n

type family NCopies n (a :: k) = (as :: [k]) | as -> n
--NCopies n (m a) = Applied m (NCopies n a)
where
NCopies Zero a = '[]
NCopies (Succ n) a = a ': NCopies n a

class ForEach n a where
foreach :: (Zn n -> a) -> HList (NCopies n a)

instance ForEach Zero a where
foreach _ = Nil

instance (Nat n, ForEach n a) => ForEach (Succ n) a where
foreach f =
f (fromJust (mkZn ((asInt @n) - 1))) ::: foreach @n @a (f . promote)

class IdApplied m n as where
idApplied :: HList (NCopies n (m as)) -> HList (Applied m (NCopies n as))

instance IdApplied m Zero as where
idApplied _ = Nil

instance IdApplied m n as => IdApplied m (Succ n) as where
idApplied (a ::: as) = a ::: idApplied @m @n @as as

+ 1
- 0
yggdrasil.cabal View File

@@ -27,6 +27,7 @@ library
Yggdrasil.Functionalities
Yggdrasil.HList
Yggdrasil.MetaProtocol
Yggdrasil.Nat
build-depends: base >= 4.11 && < 4.12
, cryptonite >= 0.25 && < 0.26
, memory >= 0.14 && < 0.15

Loading…
Cancel
Save