[Haskell-cafe] Prevent a type parameter from sharing some of its parameters with another parameter

[David Kraeutmann]

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.
>