Re: [Haskell-cafe] Class of ordered tuples

Ah, the trick is to do away with the Index class altogether and use just one instance declaration! Below I use type families because the actual index is irrelevant for the class methods. In contrast, with MultiParamTypeClasses and FunctionalDependencies the user must always explicitly give the two index parameters when invoking the class methods. With the code below, I can simply write

parse A parse (A,B) But invoking parse (B,A) results in the error message: Couldn't match type ‘'GT’ with ‘'LT’

{-# LANGUAGE TypeFamilies, DataKinds #-} module OrderedTuple where import GHC.TypeNats -- This will really be be a parser type type P a = a -> String class Range a where type Start a :: Nat type End a :: Nat parse :: P a data A = A deriving (Show) instance Range A where type Start A = 0 type End A = 0 parse = show data B = B deriving (Show) instance Range B where type Start B = 1 type End B = 1 parse = show instance (Range a, Range b, CmpNat (End a) (Start b) ~ 'LT) => Range (a,b) where type Start (a,b) = Start a type End (a,b) = End b parse (a,b) = "("++(parse a)++","++(parse b)++")"

On 16 September 2019 at 21:18 Li-yao Xia wrote:

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.