These are chat archives for unisonweb/unison

30th
Aug 2016
Paul Chiusano
@pchiusano
Aug 30 2016 14:44
after programming for a bit in the Remote monad, I’ve realized it might be nice to be able to control, via the types, where and when control is transferred to different nodes
sfultong
@sfultong
Aug 30 2016 14:45
hmm, do you have an idea for how to do that?
Paul Chiusano
@pchiusano
Aug 30 2016 14:45
probably using indexed monads
so you could write a function like:
distributed-sort : Order a -> Vector a -> Remote loc loc (Vector a)

transfer : Node -> Remote loc1 loc2 Unit
scope : Remote loc1 loc2 a -> Remote loc1 loc1 a
the signature of distributed-sort enforces that the computation must return to it’s “original” node when it completes
and the signature of transfer changes the location of the computation...
Paul Chiusano
@pchiusano
Aug 30 2016 14:51
while scope (bad name, maybe restore?) ensures that wherever the computation goes, control is returned back to its starting location
upon completion
sfultong
@sfultong
Aug 30 2016 14:51
these make sense
Paul Chiusano
@pchiusano
Aug 30 2016 14:52
you could imagine implementing scope via here and transfer
so perhaps this is a different type - newtype Remote’ loc-start loc-end a = Remote’ (Remote a)
this is a situation where dependent types would be nice
with dependent types, you could give transfer a type like (n : Node) -> Remote loc1 n Unit
so the type is very precise - it says what node you end up on
sfultong
@sfultong
Aug 30 2016 14:57
yeah, I don't have experience with indexed monads
so what are your type system dreams for unison?
I'd like to see refinement types
Paul Chiusano
@pchiusano
Aug 30 2016 14:59
i’m not sure
i like dependent types, and refinement types aren’t as expressive… but they have a good power-to-weight ratio
i had some crazy ideas a while back about being able to layer different types onto your programs
like, you could write a function once, and then give it fancier types, possibly in different type systems
Paul Chiusano
@pchiusano
Aug 30 2016 15:04
TBD
sfultong
@sfultong
Aug 30 2016 15:14
once I make my terminating language vm, you can non-termination as an effect into unison's effect system! :-P
Paul Chiusano
@pchiusano
Aug 30 2016 15:14
haha
related to non-termination, i don’t know if you’ve seen this paper, it is a classic http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.106.364&rep=rep1&type=pdf
sfultong
@sfultong
Aug 30 2016 15:25
I don't think I have...
Paul Chiusano
@pchiusano
Aug 30 2016 15:27
it’s a good one
i would say it is the paper the popularized the idea of ‘codata'
sfultong
@sfultong
Aug 30 2016 15:27
oh, interesting