[Haskell-cafe] Class of ordered tuples

[Olaf Klinke]

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 <lysxia at gmail.com> 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.
> >