[prev in list] [next in list] [prev in thread] [next in thread] 

List:       haskell-cafe
Subject:    Re: [Haskell-cafe] Class of ordered tuples
From:       Olaf Klinke <olf () aatal-apotheke ! de>
Date:       2019-09-17 8:26:57
Message-ID: 1108700783.235069.1568708817963 () webmail ! strato ! de
[Download RAW message or body]

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


[prev in list] [next in list] [prev in thread] [next in thread]