[GHC] #7495: generalizing overloaded list syntax to Sized Lists, HLists, HRecords, etc

[GHC]

#7495: generalizing overloaded list syntax to Sized Lists, HLists, HRecords, etc
-------------------------------------+-------------------------------------
        Reporter:  nwf               |                   Owner:  carter
            Type:  feature request   |                  Status:  new
        Priority:  normal            |               Milestone:  7.12.1
       Component:  Compiler          |                 Version:  7.6.1
      Resolution:                    |                Keywords:
Operating System:  Unknown/Multiple  |            Architecture:
 Type of failure:  None/Unknown      |  Unknown/Multiple
      Blocked By:                    |               Test Case:
 Related Tickets:  #9883             |                Blocking:  9883
                                     |  Differential Revisions:
-------------------------------------+-------------------------------------

Comment (by s9gf4ult):

 Hello. I propose little different solution. I dont think we should put
 methods `isNil` and `uncons` inside of this proposal, because they do not
 relate with lists construction. Here is full example of my proposal:

 {{{#!hs
 {-# LANGUAGE
   FlexibleInstances
 , TypeOperators
 , TypeFamilies
 , DataKinds
 , GADTs
   #-}

 import GHC.TypeLits

 -- | Types which can be constructed with 'cons' should instantiate this
 class Cons a where
     type Head a :: *
     type Tail a :: *
     cons :: Head a -> Tail a -> a

 -- | And types which is a empty list should instantiate this
 class Nil a where
     nil :: a


 ---------------------------------
 -- Simple homogenous lists     --
 ---------------------------------

 instance Cons [a] where
     type Head [a] = a
     type Tail [a] = [a]
     cons elem b = elem:b

 instance Nil [a] where
     nil = []

 -- | synoym for '[10, 20, 42]'
 justList :: [Int]
 justList = cons 10 $ cons 20 $ cons 42 $ nil


 -------------------------------
 -- Simple heterogenous lists --
 -------------------------------

 -- | Simple heterogenous list
 data HList (typs :: [*]) where
     HNil :: HList '[]
     HCons :: typ -> HList typs -> HList (typ ': typs)

 instance Cons (HList (t ': ts)) where
     type Head (HList (t ': ts)) = t
     type Tail (HList (t ': ts)) = HList ts
     cons = HCons

 instance Nil (HList '[]) where
    nil = HNil

 -- | synonym of '[10, 20, "hello"]'
 hlist :: HList '[Int, Integer, String]
 hlist = cons 10 $ cons 20 $ cons "hello" nil


 ---------------------------------------------------------------------------
 -- More complex heterogenous list with constraints for it's elements
 --
 ---------------------------------------------------------------------------

 -- | Checks that element contained in type list
 type family Elem (typ :: *) (typs :: [*]) :: Bool where
     Elem typ '[]             = 'False
     Elem typ (typ ': typs)   = 'True
     Elem typ1 (typ2 ': typs) = Elem typ1 typs

 -- | Heterogenous list with uniq elements
 data UniqHList (typs :: [*]) where
     UHNil  :: UniqHList '[]
     UHCons :: ('False ~ (Elem typ typs))
            => typ -> UniqHList typs -> UniqHList (typ ': typs)

 -- | Look at instance constraint, it is the same constraint as in
 -- 'UHCons' constructor
 instance ('False ~ (Elem t ts)) => Cons (UniqHList (t ': ts)) where
     type Head (UniqHList (t ': ts)) = t
     type Tail (UniqHList (t ': ts)) = UniqHList ts
     cons = UHCons

 instance Nil (UniqHList '[]) where
     nil = UHNil


 -- | This should be written as '[10, "string", 42.2, 20]'
 uniqHlist :: UniqHList '[Integer, String, Double, Int]
 uniqHlist = cons 10 $ cons "string" $ cons 42.2 $ cons 20 nil

 ---------------------------------------
 -- Vectors parametrized with length  --
 ---------------------------------------

 data Vector (len :: Nat) a where
     VNil :: Vector 0 a
     VCons :: a -> Vector len a -> Vector (len + 1) a

 -- | Look at the constraint again. It is a little hackish because GHC
 -- can not infer that __len ~ ((len - 1) + 1)__
 instance (len ~ ((len - 1) + 1)) => Cons (Vector len a) where
     type Head (Vector len a) = a
     type Tail (Vector len a) = Vector (len - 1) a
     cons = VCons

 instance Nil (Vector 0 a) where
     nil = VNil

 vector :: Vector 3 Int
 vector = cons 1 $ cons 2 $ cons 3 $ nil
 }}}

 It is compilable and contains instances for some complex cases. The method
 `cons` shoud be considered as `(:)` and `nil` should become `[]`.

 What do you think? Cheers!

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/7495#comment:11>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler