Hi Markus, This problem is complicated by the fact that the shares themselves may actually very complex implementations. We would therefore require several mkShared task derivates, for example:
mkSharedLens :: String (p -> ps) (SDSLensRead p r rs) (SDSLensWrite p w rs ws) (SDSLensNotify p w rs) (RWShared ps rs ws) -> Task (RWShared p r w) | iTask ps As an example: Somehow that feels messy. Both because every share combinator would require a wrapper, and because it relies only on convention. One upside to this solution is that the code would also have a more functional feel. Currently, shares feel a bit too much like global variables to me... The value restriction solution could probably work, even without making the type checker explicitly aware of SDSs. The Tonic compiler has support for pragmas, which could be used instead. E.g. //-# HAS_VALUE_RESTRICTION RWShared :: RWShared p r w = ... HAS_VALUE_RESTRICTION X could then mean that "any top-level value of type X and any function with result type X has a value restriction". Still, the compiler would need to be modified. > On 16 Aug 2016, at 16:58, Markus Klinik <[email protected]> wrote: > > Hi all, > > With the way Shared Data Sources are currently implemented it is possible > to write a program that first writes an integer list and then a > bool list to the same SDS. The type checker accepts this program. > > Consider the following program. The Shared Data Source s is let-bound, > which causes its type to be generalized. Later, its type can be > instantiated in different ways. > > > // begin problem.icl > module problem > import iTasks > > // Some helper functions. > // Writes a boolean list to an SDS > writeBoolList x = set [True] x > // Writes an integer list to an SDS > writeIntList x = set [1000] x > // Displays a boolean list SDS > viewBoolList :: (Shared [Bool]) -> Task [Bool] > viewBoolList x = viewSharedInformation "info" [] x > > // The actual problem. > // s is let-bound, so its type gets generalized to > // s :: forall a . Shared [a] > s = sharedStore "shared" [] > > main = > // The type of s can be instantiated to both > // Shared [Bool] and > // Shared [Int] > // in the following lines, because s is polymorphic. > writeBoolList s >>| > writeIntList s >>| > viewBoolList s > > Start world = startEngine main world > // end problem.icl > > > This problem exists in every programming language that has mutable > references and let-polymorphism. ML with its ref type introduced the > value restriction to solve this problem [1]. In Haskell, creating an MVar > is an IO action [2]. This means MVars are always lambda-bound, by the > lambdas of monadic functions, and therefore the types of MVars are never > generalized. Haskell doesn't need the value restriction. > > We could do either of those. > > The value restriction has the drawback that we must make the type checker > aware of SDSs. Constructors of SDSs must not be considered syntactic > values, while all other constructors of ADTs are. > > I think we should go in the other direction and make creation of SDSs a > task. This has the drawback that it is no longer possible to create a > global SDS and use it everywhere we need it. Instead, all SDSs must be > created in the top-level task and distributed to the subtasks as > arguments of monadic functions. This is demonstrated in the following > program. > > > // begin solution.icl > module solution > import iTasks > > // Task that creates an SDS. > // If this function were the only possibility to create an SDS, > // programmers would not be able to let-bind SDSs. > mkShared :: !String !a -> Task (Shared a) | iTask a > mkShared d x = return (sharedStore d x) > > // Same as in problem.icl > writeBoolList x = set [True] x > writeIntList x = set [1000] x > viewBoolList :: (Shared [Bool]) -> Task [Bool] > viewBoolList x = viewSharedInformation "info" [] x > > main = > // s is lambda-bound instead of let-bound, which gives the expected > // error: Type error "argument 1 of writeIntList" cannot unify demanded > // type with offered type: > // RWShared () v9 [Int] > // Shared [Bool] > mkShared "share" [] >>= \s -> > writeBoolList s >>| > writeIntList s >>| > viewBoolList s > > Start world = startEngine main world > // end solution.icl > > > This API change would require a new style of working with SDSs and we > probably need to modify every program that currently uses SDSs. But > it is a lot easier to implement than the value restriction. > > What do you think, should we do that? > > Best regards, > Markus > > [1] http://mlton.org/ValueRestriction > [2] > https://hackage.haskell.org/package/base-4.9.0.0/docs/Control-Concurrent-MVar.html > _______________________________________________ > clean-list mailing list > [email protected] > https://mailman.science.ru.nl/mailman/listinfo/clean-list _______________________________________________ clean-list mailing list [email protected] https://mailman.science.ru.nl/mailman/listinfo/clean-list
