search

idris-lang / Idris2

A purely functional programming language with first class types
https://idris-lang.org/
Other
2.46k stars 369 forks source link

[ new ] System.Concurrency.(Linear/Session) #3294

Closed gallais closed 4 weeks ago

gallais commented 1 month ago

The main takeaways are:

Combinators for parallel computing

par1 : L1 IO a -@ L1 IO b -@ L1 IO (LPair a b)
par : L IO a -@ L IO b -@ L IO (a, b)

Channels indexed by session types

send : LinearIO io =>
  (1 _ : Channel (Send ty s)) ->
  ty ->
  L1 io (Channel s)

recv : LinearIO io =>
  Channel (Recv ty s) -@
  L1 io (Res ty (const (Channel s)))

end : LinearIO io => Channel End -@ L io ()

fork : (0 s : Session) ->
       (Channel       s  -@ L IO a) -@
       (Channel (Dual s) -@ L IO b) -@
       L IO (a, b)
buzden commented 1 month ago

I'm so glad Syntax.WithProof and Data.Void are moved to base, despite this is not the main point of this PR