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
