Last active
August 29, 2015 14:17
-
-
Save aavogt/035d8e6374e50e400035 to your computer and use it in GitHub Desktop.
appending Record records
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE ScopedTypeVariables #-} | |
{-# LANGUAGE DataKinds #-} | |
{-# LANGUAGE TypeFamilies #-} | |
{-# LANGUAGE FlexibleInstances #-} | |
{-# LANGUAGE UndecidableInstances #-} | |
{-# LANGUAGE FlexibleContexts #-} | |
{-# LANGUAGE ConstraintKinds #-} | |
{-# LANGUAGE TypeOperators #-} | |
{-# LANGUAGE FunctionalDependencies #-} | |
{-# LANGUAGE TemplateHaskell #-} | |
{-# LANGUAGE QuasiQuotes #-} | |
{-# LANGUAGE MultiParamTypeClasses #-} | |
module Append where | |
import Record | |
import Language.Haskell.TH | |
import Language.Haskell.TH.Syntax | |
import Record.Types | |
import Control.Monad | |
import GHC.Exts (Constraint) | |
import GHC.TypeLits (Symbol) | |
import Data.HList.CommonMain | |
import Data.HList.HSort | |
import Data.List | |
import Record.Lens (view, Lens) | |
type HSort a b = (HSortBy1 False HLeFn a b, SameLength a b) | |
class Append a b ab where | |
append :: a -> b -> ab | |
a <+> b = append a b | |
infixr <+> | |
data FromM a | |
data FromN a | |
class ViewFrom (from :: * -> *) s nr mr a where | |
viewFrom :: Proxy from -> FieldName s -> nr -> mr -> a | |
instance Field' s mr a => ViewFrom FromM s nr mr a where | |
-- Record.Lens.view should be | |
-- view :: Lens s s a a -> s a | |
-- that avoids the ambiguity that needs an annotation here | |
viewFrom _ s n m = view (fieldLens s :: Lens mr mr a a) m | |
instance Field' s nr a => ViewFrom FromN s nr mr a where | |
viewFrom _ s n m = view (fieldLens s :: Lens nr nr a a) n | |
type family ViewFroms (fs :: [* -> *]) (sys :: [Symbol]) nr mr (as :: [*]) :: Constraint | |
type instance ViewFroms '[] '[] nr mr '[] = () | |
type instance ViewFroms (f ': fs) (sy ': sys) nr mr (a ': as) = (ViewFrom f sy nr mr a, ViewFroms fs sys nr mr as) | |
let f n m = do | |
let recNT n = case ''Record1 of | |
Name _ ng -> Name (OccName ("Record"++show n)) ng | |
recN n = case 'Record1 of | |
Name _ ng -> Name (OccName ("Record"++show n)) ng | |
ns <- replicateM n (newName "n") | |
ms <- replicateM m (newName "m") | |
nes <- replicateM n (newName "ne") | |
mes <- replicateM m (newName "me") | |
nms <- replicateM (n+m) (newName "nm") | |
nmes <- replicateM (n+m) (newName "mme") | |
nmesF <- replicateM (n+m) (newName "from") | |
let appendNM = [| \ nr mr -> | |
$(foldl (\ r (f, nm, e) -> | |
[| $r (viewFrom | |
(Proxy :: Proxy $(varT f)) | |
(undefined :: FieldName $(varT nm)) | |
nr | |
mr :: $(varT e)) |]) | |
(conE (recN (n+m))) | |
(zip3 nmesF nms nmes) | |
) |] | |
let mkApplied n ns nes = foldl (\ f (n,ne) -> [t| $f $(varT n) $(varT ne) |]) | |
(conT (recNT n)) | |
(ns `zip` nes) | |
nTy,mTy,nmTy :: TypeQ | |
nTy = mkApplied n ns nes | |
mTy = mkApplied m ms mes | |
nmTy = mkApplied (n+m) nms nmes | |
toTaggedList :: [(Name,TypeQ)] -> TypeQ | |
toTaggedList = foldr (\ (t,e) xs -> [t| Tagged $(varT t) $e ': $xs |]) [t| '[] |] | |
tnm1 :: TypeQ | |
tnm1 = toTaggedList | |
(zip (ns ++ ms) | |
((map (\e -> [t| FromN $(varT e) |]) nes) ++ | |
(map (\e -> [t| FromM $(varT e) |]) mes))) | |
tnm2 :: TypeQ | |
tnm2 = toTaggedList (nms `zip` | |
(zipWith (\ f e -> [t| $(varT f) $(varT e) |]) nmesF nmes)) | |
-- not supported... | |
viewFromCxt :: TypeQ | |
viewFromCxt = [t| ViewFroms $(toL nmesF) $(toL nms) $nTy $mTy $(toL nmes) |] | |
viewFromCxts :: [Q Pred] | |
viewFromCxts = [ classP ''ViewFrom [varT f, varT s, nTy, mTy, varT e] | |
| (f,s,e) <- zip3 nmesF nms nmes ] | |
toL :: [Name] -> TypeQ | |
toL = foldr (\ x xs -> [t| $(varT x) ': $xs |]) [t| '[] |] | |
z <- newName "z" | |
fmap (:[]) $ instanceD (sequence $ [ classP ''HSort [tnm1, tnm2], | |
varT z `equalP` nmTy] | |
++ viewFromCxts) | |
[t| Append $nTy $mTy $(varT z) |] | |
[valD (varP 'append) (normalB appendNM) []] | |
{- | |
[d| instance (HSort ok $tnm1 $tnm2, z ~ $nmTy, $viewFromCxt) => | |
Append $nTy $mTy z where | |
append = $appendNM |] | |
-} | |
in concat `fmap` sequence [ f n m | n <- [1 .. 4], m <- [1 .. 4], n+m <= 4 ] | |
type T0 = [r| { w :: () } |] | |
type T1 = [r| { x :: Int } |] | |
type T2 = [r| { y :: Char } |] | |
type T3 = [r| { z :: Double } |] | |
{- | all permutations of t0 <+> t1 <+> t2 <+> t3 | |
give the same type. | |
>>> :t _1 | |
_1 :: Record4 "w" () "x" Int "y" Char "z" Double | |
>>> :t _23 | |
_23 :: Record4 "w" () "x" Int "y" Char "z" Double | |
-} | |
t0 = [r| { w = () } |] :: T0 | |
t1 = [r| { x = 1 } |] :: T1 | |
t2 = [r| { y = 'x' } |] :: T2 | |
t3 = [r| { z = 2.4 } |] :: T3 | |
let ns = map varE ['t0 , 't1, 't2 , 't3] | |
in fmap concat $ sequence | |
$ map (\(i, e) -> [d| $(varP (mkName ("_"++show i))) = $e |]) | |
$ zip [1 .. ] | |
$ map (foldr1 (\a b -> [| $a <+> $b |])) (permutations ns) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Where can I find
Data.HList.HSort
? Google is only giving me a gist from you.