Prevent a type parameter from sharing some of its parameters with another parameter
As the title says. Motivation: in a mutable code I want to keep some parameters strictly immutable, i.e. not sharing s with the whole mutable type I think this is best illustrated by 2 examples: 1. abstract example: imagine I have a type X a b c and another type Y a b and I want to prevent any case where the first parameter of X "a" is shared with it's third parameter "c" i.e. X a b (Y a a), X a b (Y a b), X a b (Y b a), X a b (Y a d) etc., any nestings in Y referencing a etc. but allow X a b (Y b b), X a b (Y b c) and any other combination not ruled out above 2. concrete example: imagine I have a type: Item s element key where s is used in the same way as in STRef s a, i.e. it cannot leak outside of a certain context, but I want the key to be immutable i.e. independent of s under any circumstences, so I can't write a type like: Item s element (STRef s refType) this is equivalent to disallowing X a b (Y a d) in 1. Is there any way to write a restriction like this in Haskell? -- Timo
Check out TypeError from GHC.TypeLits, then make a type family or class that resolves to TypeError when both params are identical. e.g. {-# LANGUAGE TypeInType, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts #-} class CheckDistinct a b instance {-# OVERLAPS #-} TypeError (Text "Parameters must be distinct") => CheckDistinct a a instance CheckDistinct a b
:t undefined :: CheckDistinct Int Double => Int undefined :: CheckDistinct Int Double => Int :: Int
:t undefined :: CheckDistinct Int Int => Int <interactive>:1:1: error: Parameters must be distinct
On 2017-08-21 06:52, Timotej Tomandl wrote:
As the title says.
Motivation: in a mutable code I want to keep some parameters strictly immutable, i.e. not sharing s with the whole mutable type
I think this is best illustrated by 2 examples: 1. abstract example: imagine I have a type X a b c and another type Y a b and I want to prevent any case where the first parameter of X "a" is shared with it's third parameter "c" i.e. X a b (Y a a), X a b (Y a b), X a b (Y b a), X a b (Y a d) etc., any nestings in Y referencing a etc. but allow X a b (Y b b), X a b (Y b c) and any other combination not ruled out above 2. concrete example: imagine I have a type: Item s element key where s is used in the same way as in STRef s a, i.e. it cannot leak outside of a certain context, but I want the key to be immutable i.e. independent of s under any circumstences, so I can't write a type like: Item s element (STRef s refType) this is equivalent to disallowing X a b (Y a d) in 1.
Is there any way to write a restriction like this in Haskell?
-- Timo
_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.
Hi Timotej, What should happen if you capture the variable with an existential type: data E a = forall s. E (STRef s a) I guess there's not much we can do with this type anyway... Taking a complementary approach, you can write a typeclass of types that are allowed as keys. Since s is used like in ST, it must not unify with any concrete type, and there will be no instance of Allowed to be found. class Allowed a instance Allowed a => Allowed [a] instance (Allowed a, Allowed b) => Allowed (Either a b) If you can use PolyKinds and UndecidableInstances, some boilerplate can be avoided. -- Instance to traverse composite types. instance (Allowed f, Allowed a) => Allowed (f a) -- Every type constructor you can think of. instance Allowed Int instance Allowed [] instance Allowed Maybe instance Allowed Either -- etc Li-yao On 08/21/2017 06:52 AM, Timotej Tomandl wrote:
As the title says.
Motivation: in a mutable code I want to keep some parameters strictly immutable, i.e. not sharing s with the whole mutable type
I think this is best illustrated by 2 examples: 1. abstract example: imagine I have a type X a b c and another type Y a b and I want to prevent any case where the first parameter of X "a" is shared with it's third parameter "c" i.e. X a b (Y a a), X a b (Y a b), X a b (Y b a), X a b (Y a d) etc., any nestings in Y referencing a etc. but allow X a b (Y b b), X a b (Y b c) and any other combination not ruled out above 2. concrete example: imagine I have a type: Item s element key where s is used in the same way as in STRef s a, i.e. it cannot leak outside of a certain context, but I want the key to be immutable i.e. independent of s under any circumstences, so I can't write a type like: Item s element (STRef s refType) this is equivalent to disallowing X a b (Y a d) in 1.
Is there any way to write a restriction like this in Haskell?
-- Timo
_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.
Hi,
after thinking about it a bit, I think it might be necessary to provide
more context, so I opened an issue in my toy project this relates to:
https://github.com/formrre/soft-heap-haskell/issues/5
--
Timo
On Mon, Aug 21, 2017 at 5:52 AM, Timotej Tomandl
As the title says.
Motivation: in a mutable code I want to keep some parameters strictly immutable, i.e. not sharing s with the whole mutable type
I think this is best illustrated by 2 examples: 1. abstract example: imagine I have a type X a b c and another type Y a b and I want to prevent any case where the first parameter of X "a" is shared with it's third parameter "c" i.e. X a b (Y a a), X a b (Y a b), X a b (Y b a), X a b (Y a d) etc., any nestings in Y referencing a etc. but allow X a b (Y b b), X a b (Y b c) and any other combination not ruled out above 2. concrete example: imagine I have a type: Item s element key where s is used in the same way as in STRef s a, i.e. it cannot leak outside of a certain context, but I want the key to be immutable i.e. independent of s under any circumstences, so I can't write a type like: Item s element (STRef s refType) this is equivalent to disallowing X a b (Y a d) in 1.
Is there any way to write a restriction like this in Haskell?
-- Timo
participants (3)
-
David Kraeutmann -
Li-yao Xia -
Timotej Tomandl