[Haskell-cafe] Class of ordered tuples

Li-yao Xia lysxia at gmail.com
Mon Sep 16 19:18:14 UTC 2019


Hi Olaf,

 > Then the compiler rightfully complains that someone could write an 
instance Index (a,b) n


Do you expect that to happen in practice or is that only a theoretical 
possibility? (If you could tell GHC that "Index (a, b) n" is forever 
forbidden, would you?)


Have you considered using a constructor to disambiguate pairs (a, b) 
from singletons:

newtype Singleton a = Sg a

instance Index a n => Range (Singleton a) n n

or using overlapping instances and an explicit equality constraint to 
ensure that the pair instance is a "substitution instance" of the 
singleton instance:

instance {-# OVERLAPPABLE #-} (Index a n, n ~ n') => Range a n n'

or a hybrid approach with both Singleton (instead of overlap) and the 
explicit equality constraint (for more general type inference):

instance (Index a n, n ~ n') => Range (Singleton a) n n'

Cheers,
Li-yao

On 9/16/19 3:08 PM, Olaf Klinke wrote:
> Dear Cafe,
> 
> I had a lengthy discussion with GHC but so far it won't let me do the following. (Code below is simplified to transport the idea. Type families don't seem to do the trick, either.)
> A finite set of types A, B, C, ... is totally ordered. This can be expressed e.g. by a multi-parameter type class and type-level natural numbers:
> 
> instance Index A 0 where
> instance Index B 1 where
> etc.
> 
> Now I want a type class Range and an appropriate set of instance declarations that has
> A, B, (A,B), (A,C), (A,(B,C)) etc. as members but not
> (B,A) or (C,C). That is, each type appears at most once and in the defined order.
> 
> The problem is overlapping instances of the base case with the inductive case.
> 
> instance Index a n => Range a n n
> instance (Range a x y, Range b x' y', y < x') => Range (a,b) x y'
> 
> Then the compiler rightfully complains that someone could write an instance Index (a,b) n
> which would lead to conflicting instances of Range (a,b) n n. I can not make either of the type classes Index nor Range closed because there will be several of those sets of types. This problem is like smart constructors for ordered lists, but on the type level.
> 
> Thanks in advance for any hints.
> Olaf
> 	
> 
> 
> _______________________________________________
> 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.
> 


More information about the Haskell-Cafe mailing list