:)W      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~ Safe %&+,DQR% Promoted SType family for computing which types in a list of types are equal to a given type.SData type that can give us proof of membership of an element in a list of elements."Data type defining natural numbers;Type family for returning the second argument of a product. :Type family for returning the first argument of a product. {Data type that takes a kind as an argument. Its sole constructor takes two capabilities parameterized by the kind argument.cThis data type is useful if it is necessary for an indexed monad to be indexed by four parameters.  Promoted   Promoted  Promoted  ifThenElseCType family for applying zero or more constraints to types of kind J in a list of session types. It may be applied to a list of session types.CType family for applying zero or more constraints to types of kind A in a list of session types. It may be applied to a session type.CType family for applying zero or more constraints to types of kind ? in a list of session types. It may be applied to a capability.7Type family for applying a constraint to types of kind  in a list of session types.7Type family for applying a constraint to types of kind 8 in a session type. It may be applied to a session type.7Type family for applying a constraint to types of kind 6 in a session type. It may be applied to a capability.OType family for removing the receive session type from a list of session types.sType family for removing the receive session type from the given session type. It may be applied to a session type.qType family for removing the receive session type from the given session type. It may be applied to a capability.LType family for removing the send session type from a list of session types.pType family for removing the send session type from the given session type. It may be applied to a session type.nType family for removing the send session type from the given session type. It may be applied to a capability.@Type family for calculating the dual of a list of session types.eType family for calculating the dual of a session type. It may be applied to the actual session type.ZType family for calculating the dual of a session type. It may be applied to a capability.We made  injective to support calculating the dual of a selection that contains an ambiguous branch. Of course that does require that the dual of that ambiguous branch must be known.)Retrieves the context from the capability.Retrieves the session type from the capability[A capability that stores a context/scope that is a list of session types and a session type The session type data type<Each constructor denotes a specific session type. Using the  DataKinds3 pragma the constructors are promoted to types and   is promoted to a kind.! Send a value" Recv a value#Selection of branches$Offering of branches%Delimit the scope of recursion&Weaken the scope of recursion'Recursion variable(End of the session+  !"#$%&'()  %'!"#$&() !"#$%&'(    !"#$%&'(!6"6Safe+9;<=?D ,<Type class for indexed monads that may lift IO computations..DType class for indexed monads that may mask asynchronous exceptions./run an action that disables asynchronous exceptions. The provided function can be used to restore the occurrence of asynchronous exceptions.0PEnsures that even interruptible functions may not raise asynchronous exceptions.1>Type class for indexed monads to allow catching of exceptions.2&Provide a handler to catch exceptions.3@Type class for indexed monads in which exceptions may be thrown.4 Provide an  to be thrown50Type class representing the indexed monad reader93Type class for lifting indexed monadic computations;+Type class for lifting monadic computations,-./0123456789:;<=>?@ABCDEFGH      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~,-./0123458769:;<=A>?@BCDEFGHEFBCD=>?@A;<9:56783412./0,-HG ,-./0123456789:;<=>?@ABCDEFGH>1?1Safe%&+,9:;<=?DQRTI4Type class for selecting a branch through injection.=Selects the first branch that matches the given session type. prog :: MonadSession m => m ('Cap ctx (Sel '[Eps, String :!> Eps, Int :!> Eps])) ('Cap ctx Eps) () prog = sel >> send "c" >>= eps ;It should be obvious that you cannot select a branch using J? if that branch has the same session type as a previous branch.KThe KZ type class exposes a set of functions that composed together form a session typed programA type that is an instance of K' must therefore also be an instance of =.NThe functions themselves are generally defined as wrappers over corresponding STTerm constructors.VaA session typed program that is polymorphic in its context can often not be used by interpreters. We can apply Vk to the session typed program before passing it to an interpreter to instantiate that the context is empty.W!Monadic composable definition of VVPrefix a session typed program with (empty >>) to instantiate the context to be empty.XAllows indexing of selections. The given e type can be used as an indexed to select a branch. This circumvents the need to sequence a bunch of N and O to select a branch. prog :: MonadSession m => m ('Cap ctx (Sel '[a,b,c,d])) ('Cap ctx Eps) () MonadSession m => m ('Cap ctx b) ('Cap ctx Eps) () prog2 = prog >> selN (RefS RefZ) Y'Select the first branch of a selection.Z(Select the second branch of a selection.['Select the third branch of a selection.\(Select the fourth branch of a selection.]VTakes two session typed programs and constructs an offering consisting of two branches^Infix synonym for Q_Infix synonym for ] Using both ^ and _- we can now construct an offering as follows: / branch1 <& branch2 <& branch3 <&> branch4 This will be parsed as 3(branch1 <& (branch2 <& (branch3 <&> branch4))) `#A fixpoint combinator for recursionvThe argument function must take a recursion variable as an argument that can be used to denote the point of recursion. For example: &prog = recurseFix \f -> do send 5 f @This program will send the number 5 an infinite amount of times.a!Monadic composable definition of Rb!Monadic composable definition of Sc!Monadic composable definition of Td!Monadic composable definition of U!IJKLMNOPQRSTUVWXYZ[\]^_`abcdefgIJKLMNOPQRSTUVWXYZ[\]^_`abcdKLMNOPQRSTUVWXYZ[\IJ^_]`abcdIJK LMNOPQRSTUVWXYZ[\]^_`abcdefg^1_2None +,69;DQRTEType class that places the nodes at the correct locations in the grid2Determines size of grid based on the session typeshGType class for constructing a diagram that visualizes the session types*We use a State monad to modify the diagramUsed to make unique nameNumber of weakeningscurrent position in the gridDiagram that we buildGrid that will contain nodes i'Visualizes the session type of a given STTerm0 You may use this function in the following way main = visualize stKThen the following command will generate a diagram named "sessiontype.png"  7stack exec vis-sessiontype -- -o sessiontype.png -w 400EFor more information on how to generate a diagram please visit the  ,https://hackage.haskell.org/package/diagramsdiagrams packagej3Visualizes a given session type denoted by a Proxy.Returns a unique nameName a given node<Checks the current position and returns the name of the nodeReturns current location/Update the current location with a new locationMove up by oneMove down by oneMove to the right by oneKeep moving to the right until!Increase the number of weakenings!decrease the number of weakenings Get current number of weakenings)Insert new number of weaknings into stateReturns the gridSaves a new gridReturns the diagramSaves a new diagram$Place a node at the current location"Place a node at the given locationph      ij!"#$%&'()*+,-./0123456789:;<=>?@ABklmnopqrstuvwxyz{|}~hijijhUh        ij!"#$%&'()*+,-./0123456789:;<=>?@ABklmnopqrstuvwxyz{|}~Safe %&+,/9;<=DQR The STTerm GADTAlthough we say that a O is annotated with a session type, it is actually annotated with a capability ().WThe capability contains a context that is necessary for recursion and the session type.;The constructors can be split in four different categories:Communication:  and  for basic communication Branching: , ,  and  Recursion: ,  and Unsession typed:  and RThe constructor for sending messages. It is annotated with the send session type (").UIt takes as an argument, the message to send, of type equal to the first argument of " and the continuing 3 that is session typed with the second argument of ".WThe constructor for receiving messages. It is annotated with the receive session type (!)eIt takes a continuation that promises to deliver a value that may be used in the rest of the program.5Selects the first branch in a selection session type.KBy selecting a branch, that selected session type must then be implemented.+Skips a branch in a selection session type.gIf the first branch in the selection session type is not the one we want to implement then we may use  to skip this.4Dually to selection there is also offering branches.Unlike selection, where we may only implement one branch, an offering asks you to implement all branches. Which is chosen depends on how an interpreter synchronizes selection with offering.BThis constructor denotes the very last branch that may be offered.Doffers a branch and promises at least one more branch to be offered.1Constructor for delimiting the scope of recursion]The recursion constructors also modify or at least make use of the context in the capability.The 2 constructor inserts the session type argument to %+ into the context of the capability of its  argument.This is necessary such that we remember the session type of the body of code that we may want to recurse over and thus avoiding infinite type occurrence errors.;Constructor for weakening (expanding) the scope of recusion&This constructor does the opposite of %, by popping a session type from the context.4Use this constructor to essentially exit a recursion/Constructor that denotes the recursion variableIt assumes the context to be non-empty and uses the session type at the top of the context to determine what should be implemented after .Constructor that makes  a (indexed) monadConstructor that makes  a (indexed) monad transformer+This function can be used if we do not use lift. in a program but we must still disambiguate m. Safe%&,QRT>For this function tThe user will act as the dual to the given W. User interaction is only required when the given program does a receive or an offer.'A possible interaction goes as follows: Nprog = do send 5 x <- recv offer (eps x) (eps "") main = interactive prog C> Enter value of type String: "test" > (L)eft or (R)ight: L "test"Different from h is that this function gives the user the choice to abort the session after each session typed action. ]Furthermore, it also prints additional output describing which session typed action occurred.CDECDESafe+,9:;<=?DOQRT"Type class for flattening branches The function  takes and traverses a . If it finds a branching session type that has a branch starting with another branching of the same type, then it will extract the branches of the inner branching and inserts these into the outer branching. This is similar to flattening a list of lists to a larger list. For example: Sel '[a,b, Sel '[c,d], e]becomes Sel '[a,b,c,d,e]hThis only works if the inner branching has the same type as the outer branch (Sel in Sel or Off in Off).nAlso, for now this rewrite only works if one of the branching of the outer branch starts with a new branching. For example:  Sel '[a,b, Int :!> Sel '[c,d],e]does not become "Sel '[a,b,Int :!> c, Int :!> d, e]3This is something that will be added in the future.2Type class for eliminating unused recursive types. The function  traverses a given H. While doing so, it will attempt to remove constructors annotated with % or &N from the program if in doing so does not change the behavior of the program.CFor example, in the following session type we may remove the inner % and the &.   R (R (Wk V))We have that the outer %6 matches the recursion variable because of the use of &. That means the inner %, does not match any recursion variable (the %W is unused) and therefore may it and its corresponding constructor be removed from the  program.We also remove the &@, because the session type pushed into the context by the inner % has also been removed.The generated session type is R VType class for rewriting an  to its normal formnThe type class has a single instance that is constrained with two type classes. One for each type of rewrite.>FGHIJKLMNOPQRSTUVWXYZ[\]^9FGHIJKLMNOPQRSTUVWXYZ[\]^Safe)OTWe define an indexed codensity monad that allows us to reduce quadratic complexity from repeated use of (>>=) in a session typed program to linear complexity. Turns the $ representation of a program to the  representation.The idea is to apply  on a  program to make the resulting  program more efficient.Transforms an  program into a  representation.ONote that applying this function to a session typed program and then applying * to the result will not be more efficient.This is because applying & already induces quadratic complexity.   SafeR  %'!"#$&(IJKLMNOPQRSTUVWXYZ[\]^_`abcdRKLMNOPQRSTUVWXYZ[\IJ^_]`abcd !"#$%&'(  Safe %&,/DQR The < data type describes the session type actions that were done We use the I data type to supply input for the receives in a session typed programs.We annotate a 3 with a capability for the following three reasons: Each M( may return a value of a different type.\Given reason 1 and that we can have branching, we must also be able to branch in the stream.TWe can now write a function that recursively generates input for a recursive program Similar to , ^ has a constructor for each session type. Each constructor takes an argument that is another  type, except for D that takes an additional argument that will be used as input, and $ that denotes the end of the stream.sAt first it might be confusing which constructors and in what order these constructors should be placed to form a $ that can be used as input for some ..This is actually not that difficult at all. A R is session typed and that session type must be equal to the session type of the (. As such one merely needs to create a c that has the same session type and if you don't the type checker will tell you what it incorrect.EThere are two things that you need to be aware of when constructor a .The  constructors for offering (S_OffZ and S_OffS) require that you define input for all branches of the offering. This can be quite cumbersome, so we include a  and , constructor that behave similarly to  and . You are not guaranteed that a < can be used for all session typed programs that have the same session type. Specifically when it comes to selection can we not guarantee this. The session type for selection only tells us about which branches could be selected. It does not tell us which branch was selected as this is runtime dependent.Purely evaluates a given  using the input defined by .UThe output is described in terms of the session type actions within the given program7An example of how to use this function goes as follows:  prog :: STTerm Identity ('Cap '[] (Int :!> String :?> Eps)) ('Cap '[] Eps) String prog = send 5 >> recv >>= eps strm = S_Send $ S_Recv "foo" S_Eps  run prog strm%O_Send 5 $ O_Recv "foo" $ O_Eps "foo"tInstead of describing the session typed actions, it returns a list of the results of all branches of all offerings. 8prog = offer (eps 10) (eps 5) strm = S_OffS S_Eps S_Eps runAll prog strm[10,5]Same as  but applies  to the resulting listrunSingle prog strm10o cannot deal with lifted computations. This makes it limited to session typed programs without any use of lift.iThis function allows us to evaluate lifted computations, but as a consequence is no longer entirely pure.Monadic version of .Monad version of _(Extracts all result values from a given 6`a_bcdefghijklmnopq!! `a_bcdefghijklmnopqr    !"#$%&'())*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~                                   !"#$%&%'%(%)%*%+%,%-%.%/%0%1%2%3%4%5%6%7%89:;<=>?@ABCDEFGHIHJHKHLHMHNHHOPQRSTUVWXYXZX[\]%^%_%`%a%b%c%d%e%f%g%h%i%j%k%lmnopqrstsusvswxyz{|{}{~{{{{{{{{{{s            {{{{{{{{{XXssss  H      !"#$%&'()*+,--./0123456789:;<==>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~                   )sessiontypes-0.1.0-DWOrnOR7fQP7Kzb9x4zPQ6Control.SessionTypes.TypesControl.SessionTypes.Indexed!Control.SessionTypes.MonadSessionControl.SessionTypes.VisualizeControl.SessionTypes.STTerm Control.SessionTypes.InteractiveControl.SessionTypes.NormalizeControl.SessionTypes.CodensityControl.SessionTypes.DebugControl.SessionTypesAppend TypeEqListRefRefZRefSNatZSRightLeftProd:*:OrNot IfThenElseHasConstraintsHasConstraintSTMapHasConstraint HasConstraint RemoveRecvST MapRemoveRecv RemoveRecv MapRemoveSend RemoveSendST RemoveSendMapDualDualSTDualGetCtxGetSTCapST:?>:!>SelOffRWkVEps $fShowNat$fEqNat$fOrdNat IxMonadIOliftIO IxMonadMaskmaskuninterruptibleMask IxMonadCatchcatch IxMonadThrowthrowM IxMonadReaderasklocalreader IxMonadIxTiliftIxMonadTliftIxMonad>>=>>returnfail IxApplicativepure<*> IxFunctorfmap ifThenElseapSelectsel MonadSessionsendrecvsel1sel2offZoffSrecurseweakenvarepsemptyempty0selNselN1selN2selN3selN4offer<&<&> recurseFixrecurse0weaken0var0eps0$fSelect'[]:t:$fSelect'[]:s: $fSelectxss MkDiagram visualize visualizeP$fPlaceNodeskEps$fPlaceNodeskWk$fPlaceNodeskV$fPlaceNodeskR$fPlaceNodeskOff$fPlaceNodeskOff0$fPlaceNodeskSel$fPlaceNodeskSel0$fPlaceNodesk:?>$fPlaceNodesk:!>$fCoordinateskEps$fCoordinateskWk$fCoordinateskV$fCoordinateskR$fCoordinateskOff$fCoordinateskOff0$fCoordinateskSel$fCoordinateskSel0$fCoordinatesk:?>$fCoordinatesk:!> $fMkDiagramks $fEqNodeType$fShowNodeTypeSTTermSendRecvSel1Sel2OffZOffSRecWeakenVarRetLift inferIdentity$fMonadSessionSTTerm$fIxMonadIOCapSTTerm$fIxMonadTCapSTTermm$fIxMonadCapSTTerm$fIxApplicativeCapSTTerm$fIxFunctorCapSTTerm $fMonadSTTerm$fApplicativeSTTerm$fFunctorSTTerm interactiveinteractiveStepFlattenflattenElimRecelimRec Normalize normalize$fFlatten'CapaCapCapCap$fFlatten'CapaCapCapCap0$fFlatten'CapaCapCapCap1$fFlatten'CapaCapCapCap2$fFlatten'kaCapCaprwl$fFlatten'kaCapCaprwl0$fFlatten'CapaCapCapCap3$fFlatten'CapaCapCapCap4$fFlatten'CapaCapCapCap5$fFlatten'CapaCapCapCap6$fFlatten'CapaCapCapCap7$fFlatten'CapaCapCapCap8$fFlatten'CapaCapCapCap9$fFlatten'CapaCapCapCap10$fFlatten'CapaCapCapCap11$fFlatten'CapaCapCapCap12 $fFlattenass'$fElimRec'aCapCapCap$fElimRec'aCapCapCap0$fElimRec'aCapCapCap1$fElimRec'aCapCapCap2$fElimRec'aCapCapCap3$fElimRec'aCapCapCap4$fElimRec'aCapCapCap5$fElimRec'aCapCapCap6$fElimRec'aCapCapCap7$fElimRec'aCapCapCap8$fElimRec'aCapCaprml$fElimRec'aCapCaprml0 $fElimRecass'$fNormalizeaass''IxCrunIxCabsrep$fMonadSessionIxC$fIxMonadCapIxC$fIxApplicativeCapIxC$fIxFunctorCapIxCOutputO_SendO_RecvO_Sel1O_Sel2O_OffZO_OffSO_Off1O_Off2O_RecO_VarO_WeakenO_EpsO_LiftStreamS_SendS_RecvS_Sel1S_Sel2S_OffZS_OffSS_Off1S_Off2S_RecS_WeakenS_VarS_EpsrunrunAll runSinglerunMrunAllM runSingleM$fNFDataStream$fNFDataOutput $fEqStream $fShowStream $fEqOutput $fShowOutputbaseGHC.Base++ghc-prim GHC.Classes||notMapHasConstraints GHC.TypesTypeHasConstraintsST GHC.Exception ExceptionGHC.PrimseqGHC.Listfilterzip System.IOprint Data.Tuplefstsnd otherwisemap$GHC.Real fromIntegral realToFracGHC.EnumBoundedminBoundmaxBoundEnumenumFrom enumFromThenenumFromThenTo enumFromTofromEnumtoEnumsuccpredEq==/= GHC.FloatFloatingpiexplogsqrt**logBasesincostanasinacosatansinhcoshtanhasinhacoshatanh Fractional fromRational/recipIntegral toIntegerquotremdivmodquotRemdivModMonadFunctor<$GHC.NumNum*+-negate fromIntegersignumOrd>=minmax><<=compareGHC.ReadRead readsPrecreadListReal toRational RealFloat floatRadix floatDigits floatRange decodeFloat encodeFloatexponent significand scaleFloatisNaN isInfiniteisDenormalizedisNegativeZeroisIEEEatan2RealFracproperFractiontruncateroundceilingfloorGHC.ShowShowshow showsPrecshowList Applicative*><* Data.FoldableFoldablefoldMaplengthfoldrnullfoldlfoldl1sumproductfoldr1maximumminimumelemData.Traversable TraversabletraversemapM sequenceAsequenceMonoidmemptymappendmconcatBoolFalseTrueCharDoubleFloatInt integer-gmpGHC.Integer.TypeIntegerMaybeNothingJustOrderingLTEQGTRationalIOWord Data.EitherEitherGHC.ErrerrorideitherStringShowSreadIOreadLn appendFile writeFilereadFileinteract getContentsgetLinegetCharputStrLnputStrputChar Text.ReadreadreadsGHC.IO.ExceptionioErrornotElemallanyorand concatMapconcat sequence_mapM_GHC.IOFilePath userErrorIOError Data.OldListunwordswordsunlineslineslex readParenText.ParserCombinators.ReadPReadS Data.Functor<$>lcmgcd^^^oddeven showParen showStringshowCharshowsunzip3unzipzipWith3zipWithzip3!!lookupreversebreakspansplitAtdroptake dropWhile takeWhilecycle replicaterepeatiteratescanr1scanrscanl1scanlinitlasttailhead Data.MaybemaybeuncurrycurrysubtractasTypeOfuntil$!flip.const=<< undefinederrorWithoutStackTrace&&Select'sel' PlaceNodes CoordinatesDiagramMcounterweakenNlocdiaggridnewNamenameNode getNameAtCurrgetLocsaveLocincrLocYdecrLocYincrLocX incrLocXWhileincrWkdecrWkgetWksaveWkgetGridsaveGridgetDiagsaveDiag placeAtCurrM placeAtLocM placeNodesgetXgetY mkDiagramDState Orientation HorizontalVerticalNodeTypeN_SendN_RecvN_BN_AnchN_CRN_EndN_EmpTN_RN_VN_WNodenamenodeTypenodeDiagGridnewGrid gridIndex gridIndex'diagSizenewDiag pointDiagarrBetween_noHeadsendNoderecvNodeendNodeempNodecrNodeanchNodeoffNodeselNoderNodevNodewNodeencasetypeBox newDState runDiagramM gridToDiagram placeAtLoc printGridoperationDiagram branchDiagram placeAnchors connectGrid connectNodeswalkGridconnectRecursions backTrackrToLeftinteractiveStep'printSTwaitStepMapRewriteTypes RewriteTypesRewriteFlattenListRewritesSTMapListRewritesCtx ListRewritesFlatten'flatten'MapApplyElimRecPathApplyElimRecPath MapMergePath MergePathMapDeleteWkPath DeleteWkPath HasPathToV KeepWkPath KeepRPathMapElimRecAllPathElimRecAllPathSTElimRecAllPathElimRec'elimRec' singleSel instSelApp instSelPrep evalOutputrun'runM'rec2rec4rec8rec16rec32rec64rec128rec100wk2wk4wk8wk16wk32wk64wk128wk100