From: Nathaniel Wesley Filardo <nwf@cs.jhu.edu>
Date: Wed, 9 Jan 2013 19:54:26 +0000 (-0500)
Subject: More foolishness with sexy types
X-Git-Url: https://hydra-www.ietfng.org/gitweb/?a=commitdiff_plain;h=029c59097212910b5e7464a5576cc4e77e3c215a;p=dyna2

More foolishness with sexy types
---

diff --git a/src/Dyna/XXX/HList.hs b/src/Dyna/XXX/HList.hs
index ab2983c..4ca2865 100644
--- a/src/Dyna/XXX/HList.hs
+++ b/src/Dyna/XXX/HList.hs
@@ -9,6 +9,7 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE NoImplicitPrelude #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE Rank2Types #-}
@@ -28,11 +29,29 @@ module Dyna.XXX.HList(
   HRList(..), hrlmapa, hrllen, hrlmap, hrlproj, hrlTravProj,
 
   -- * Interoperation between HList and HRList
-  HLR(..), hlToHrl,
+  HLR(..), HLRFunc(..), hlToHrl,
 ) where
 
-import           Control.Applicative
+import           Prelude (Eq(..),Ord(..),Show(..),
+                          Bool(..),(&&),
+                          Ordering(..),
+                          Int,(+),
+                          (++),
+                          seq)
+import           Control.Applicative (Applicative,pure,liftA2)
 import           GHC.Prim (Constraint)
+import qualified GHC.TypeLits as TL
+
+------------------------------------------------------------------------}}}
+-- Rebind List Syntax                                                   {{{
+
+{-
+infixr 5 :
+
+class ListOp a e where
+  ([]) :: a
+  (:)  :: e -> a -> a
+-}
 
 ------------------------------------------------------------------------}}}
 -- Type-level functions                                                 {{{
@@ -42,6 +61,7 @@ type family Append (x :: [k]) (y :: [k]) :: [k]
 type instance Append '[] y = y
 type instance Append (x ': xs) y = x ': Append xs y
 
+
 -- | Compute the type of an HList subject to some type function
 type family Map (f :: k -> k') (x :: [k]) :: [k']
 type instance Map f '[] = '[]
@@ -52,6 +72,21 @@ type family UnMap (f :: k -> k') (x :: [k']) :: [k]
 type instance UnMap f '[] = '[]
 type instance UnMap f (f a ': fas) = a ': UnMap f fas
 
+{-
+-- | Filter
+type family Filter (f :: k -> Bool) (xs :: [k]) :: [k']
+type instance Filter f '[] = '[]
+type instance Filter f (x ': xs) = MaybeCons (f x) x (Filter f xs)
+
+type family MaybeCons (mk :: Bool) (x :: k) (xs :: [k]) :: [k]
+type instance MaybeCons False x xs = xs
+type instance MaybeCons True  x xs = x ': xs
+-}
+
+type family Length (x :: [k]) :: TL.Nat
+type instance Length '[] = 0
+type instance Length (x ': xs) = 1 TL.+ (Length xs)
+
 -- | Apply a type function yielding a constraint to each element of a
 -- lifted list.
 type family MapConstraint (f :: k -> Constraint) (x :: [k]) :: Constraint
@@ -62,7 +97,7 @@ type instance MapConstraint f (x ': xs) = (f x, MapConstraint f xs)
 -- Classes                                                              {{{
 
 -- | Assert that two lifted-lists are of the same length
-class EqLen (x :: [k]) (y :: [k']) | x -> y, y -> x
+class EqLen (x :: [k]) (y :: [k'])
 instance EqLen '[] '[]
 instance (EqLen xs ys) => EqLen (x ': xs) (y ': ys)
 
@@ -80,6 +115,16 @@ instance Show (HList '[]) where show _ = "HN"
 instance (Show a, Show (HList as)) => Show (HList (a ': as)) where
     show (a :+ as) = show a ++ " :+ " ++ show as
 
+instance Eq (HList '[]) where _ == _ = True
+instance (Eq a, Eq (HList as)) => Eq (HList (a ': as)) where
+    (a :+ as) == (b :+ bs) = a == b && as == bs
+
+instance Ord (HList '[]) where compare _ _ = EQ
+instance (Ord a, Ord (HList as)) => Ord (HList (a ': as)) where
+    compare (a :+ as) (b :+ bs) = case compare a b of
+        EQ -> compare as bs
+        x  -> x
+
 hlmapa :: (Applicative m, Map c t ~ t')
        => (forall a . a -> m (c a)) -> HList t -> m (HList t')
 hlmapa _ HN = pure HN
@@ -101,13 +146,13 @@ infixr 5 :++
 
 -- | A heterogenous list in which every element is the image of some
 -- type-function @r :: * -> *@.
-data HRList r a where
+data HRList (r :: k -> *) (a :: [k]) where
  HRN   :: HRList r '[]
  (:++) :: r a -> HRList r b -> HRList r (a ': b)
 
 instance Show (HRList r '[]) where show _ = "HRN"
 instance (Show (r a), Show (HRList r as)) => Show (HRList r (a ': as)) where
-    show (a :++ as) = show a ++ " :+ " ++ show as
+    show (a :++ as) = show a ++ " :++ " ++ show as
 
 hrllen :: HRList r t -> Int
 hrllen = go 0
@@ -143,8 +188,14 @@ hlToHrl :: (forall b . b -> r b) -> HList a -> HRList r a
 hlToHrl _ HN = HRN
 hlToHrl f (a:+as) = f a :++ (hlToHrl f as)
 
-class (Map r a ~ ra, UnMap r ra ~ a)
-   => HLR (r :: * -> *) (a :: [*]) (ra :: [*])
+class (Map r a ~ ra, UnMap r ra ~ a) => HLR (r :: k -> k') (a :: [k]) (ra :: [k'])
+instance HLR r '[] '[]
+instance (ra ~ r a, HLR r as ras) => HLR r (a ': as) (ra ': ras)
+
+-- | Kind-restricted version of HLR that offers functionality for
+-- manipulating data.
+class (HLR r a ra)
+   => HLRFunc (r :: * -> *) (a :: [*]) (ra :: [*])
  where
   -- | Reinterpret an HList as an HRList
   hlAsHrl :: HList ra -> HRList r a
@@ -152,12 +203,12 @@ class (Map r a ~ ra, UnMap r ra ~ a)
   hrlAsHl :: HRList r a -> HList ra
   -- | Derive an HList by unwrapping each element.
   hrlToHl :: (forall b . r b -> b) -> HRList r a -> HList a
-instance HLR r '[] '[]
+instance HLRFunc r '[] '[]
  where
   hlAsHrl _ = HRN
   hrlAsHl _ = HN
   hrlToHl _ _ = HN
-instance (ra ~ r a, HLR r as ras) => HLR r (a ': as) (ra ': ras)
+instance (ra ~ r a, HLRFunc r as ras) => HLRFunc r (a ': as) (ra ': ras)
  where
   hlAsHrl (a :+ as) = a :++ hlAsHrl as
   hrlAsHl (a :++ as) = a :+ hrlAsHl as
diff --git a/src/Dyna/XXX/THTupleInternals.hs b/src/Dyna/XXX/THTupleInternals.hs
index 8b20c90..abb78f9 100644
--- a/src/Dyna/XXX/THTupleInternals.hs
+++ b/src/Dyna/XXX/THTupleInternals.hs
@@ -42,9 +42,7 @@ promoteList = foldr pcp promotedNilT
 mkMKLT :: Name -> Int -> Q Dec
 mkMKLT _mklt n = do
   names <- mkNames n
-
-  tySynInstD _mklt [promoteList $ map varT names]
-                 $ mkTy n names
+  tySynInstD _mklt [tySynEqn [promoteList $ map varT names] $ mkTy n names]
 
 mkMKLTs t = foreachTupleSize (mkMKLT t)
 
@@ -53,8 +51,7 @@ mkMKRLT _mklrt n = do
   names <- mkNames n
   vr <- liftM varT $ newName "r"
 
-  tySynInstD _mklrt [vr, promoteList $ map varT names]
-                  $ mkRTy n vr names
+  tySynInstD _mklrt [tySynEqn [vr, promoteList $ map varT names] $ mkRTy n vr names]
 
 mkMKRLTs t = foreachTupleSize (mkMKRLT t)
 
@@ -68,14 +65,15 @@ mkTyMap nargs _ty _fn = do
 
   args <- liftM (map varT) $ mkNames nargs
 
-  nil  <- tySynInstD _ty (args++[promotedNilT]) promotedNilT
+  nil  <- tySynInstD _ty [tySynEqn (args++[promotedNilT]) promotedNilT]
 
   x  <- liftM varT $ newName "x"
   xs <- liftM varT $ newName "xs"
   let afn = genMap appT fn id args
   let aty = genMap appT ty id args
 
-  cons <- tySynInstD _ty (args++[pcp x xs]) $ pcp (afn `appT` x) (aty `appT` xs)
+  cons <- tySynInstD _ty [ tySynEqn (args++[pcp x xs])
+                         $ pcp (afn `appT` x) (aty `appT` xs) ]
   return [nil,cons]
 
 mkTyMapFlatN :: Int -> Name -> Name -> Int -> Q Dec
@@ -87,10 +85,10 @@ mkTyMapFlatN nargs _ty _fn size = do
   args <- liftM (map varT) $ mkNames nargs
   let afn = genMap appT fn id args
 
-  tySynInstD _ty (args++[promoteList $ map varT names])
-               $ genMap appT (conT $ tupleTypeName size)
-                 (appT afn . varT)
-                 names
+  tySynInstD _ty [ tySynEqn (args++[promoteList $ map varT names])
+                 $ genMap appT (conT $ tupleTypeName size)
+                   (appT afn . varT)
+                   names ]
 
 -- | The composition mkTyMap (MKLT a)
 mkTyMapFlat a b c = foreachTupleSize (mkTyMapFlatN a b c)
@@ -104,9 +102,9 @@ mkTyUnMapN _mwr nargs _ty _fn size = do
   args <- liftM (map varT) $ mkNames nargs
   let afn = genMap appT fn id args
 
-  tySynInstD _ty (args++[mkTy size names])
+  tySynInstD _ty [ tySynEqn (args++[mkTy size names])
                  $ maybe id (\_wr -> appT (conT _wr)) _mwr
-                 $ promoteList $ map (appT afn . varT) names
+                 $ promoteList $ map (appT afn . varT) names ]
 
 mkTyUnMap a b c d = foreachTupleSize (mkTyUnMapN a b c d)
 
@@ -136,8 +134,8 @@ mkTupleInstance _tc _rter _tol _hc _hn _thl _lth _opr _oprs n | n > 1 = do
                    $ map varP names
 
   instanceD (cxt []) (appT (conT _tc) ty) -- where
-            [tySynInstD _rter [ty, vr] $ mkRTy n vr names
-            ,tySynInstD _tol [ty] $ promoteList $ map varT names
+            [tySynInstD _rter [tySynEqn [ty, vr] $ mkRTy n vr names]
+            ,tySynInstD _tol [tySynEqn [ty] $ promoteList $ map varT names]
             ,funD _thl  [clause [rpa] (normalB $ lrpa) [] ]
             ,funD _lth  [clause [plpa] (normalB $ tupE $ map varE names) [] ]
             ,funD _opr  [clause [varP f, rpa] (normalB $ frpa) [] ]
@@ -164,8 +162,8 @@ mkRTupleInstance _tc _rte _rtr _opel n | n > 1 = do
   let rpa = tupP $ map varP names
   let lfrpa = listE fnames
   instanceD (cxt []) (appT (conT _tc) rty) -- where
-            [tySynInstD _rtr [rty] vr
-            ,tySynInstD _rte [rty] $ mkTy n names
+            [tySynInstD _rtr [tySynEqn [rty] vr]
+            ,tySynInstD _rte [tySynEqn [rty] $ mkTy n names]
             ,funD _opel [clause [varP f, rpa] (normalB $ lfrpa) [] ]
             ]