lookup fields in nested records as if they are actually flat (by enumerating all paths through the nested records)

Main.hs

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverlappingInstances #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Main (main) where

import GHC.Exts
import GHC.TypeLits
import Data.Proxy
import Data.Type.Equality


-- * each data type needs to define
data P a b = P { p1 :: a, p2:: b }
       deriving Show

instance SetGet "p1" (P a b) a where
    get _ = p1

instance SetGet "p2" (P a b) b where
    get _ = p2

instance FieldList1 (P a b) '[ "p1", "p2" ] True


-- ** then getDeep can be used to get the field nested inside which
-- provides the right result type

{- |

>>> main
"a"
"b"
'b'
'a'

-}
main = do
    let w = P (P "a" 'a') (P 'b' "b")
        printChar x = print (x :: Char)
        printStr  x = print (x :: String)

        printP :: (Show a, Show b) => P a b -> IO ()
        printP x = print x

        pp1 = Proxy :: Proxy "p1"
        pp2 = Proxy :: Proxy "p2"

    -- the combination of desired result type (String or Char)
    -- as well as the label p1 or p2 uniquely determines what
    -- part of w to print
    printStr  $ getDeep pp1 w
    printStr  $ getDeep pp2 w
    printChar $ getDeep pp1 w
    printChar $ getDeep pp2 w

{- {-
    the following two dont work but I think they should.
    the problem seems to be that
    
    Proxy :: Proxy (P a b == String)
    
    doesn't get simplified to
    
    Proxy :: Proxy False
    
    GHC should be able to see that without having
    to specify concrete values for the type variables
    'a' and 'b'
    -}

    printP $ getDeep pp1 w
    printP $ getDeep pp2 w
    -}


-- * and the implementation

class FilterSGP (r :: *) (v :: *) (xs :: [[Symbol]]) (xs' :: [[Symbol]]) | r v xs -> xs'

instance FilterSGP r v '[] '[]

instance (SetGetPath n r v',
          ConsTrue (v == v') n out1 ~ out,
          FilterSGP r v ns out1)
    => FilterSGP r v (n ': ns) out


type family ConsTrue (b :: Bool) (x :: k) (xs :: [k]) :: [k]
type instance ConsTrue True x xs = x ': xs
type instance ConsTrue False x xs = xs

class SetGet (x :: Symbol) r v | x r -> v where
    -- set :: Proxy x -> v -> r -> r
    get :: Proxy x -> r -> v


class SetGetPath (xs :: [Symbol]) r v | xs r -> v where
    getPath :: Proxy xs -> r -> v

instance (SetGet x r s, SetGetPath xs s v) => SetGetPath (x ': xs) r v where
    getPath _ = getPath (Proxy :: Proxy xs) . get (Proxy :: Proxy x)

instance SetGetPath '[] r r where
    getPath _ r = r


getDeep :: forall (path :: [Symbol]) r v (paths :: [[Symbol]]) (n :: Symbol).
   (FilterSGP r v (FilterLastEq n paths) '[ path ],
        -- probably want to use GHC.TypeLits.TypeError
        -- to point out cases like:
        --    * the label n isn't at the end of any of the paths
        --    * there are multiple or zero paths that give the desired v
    SetGetPath path r v,
    FieldTree r paths) =>
    Proxy n -> r -> v
getDeep _ = getPath (Proxy :: Proxy path)


testFieldTree1 :: FieldTree (P (P [Char] Char) (P Char [Char])) r => Proxy r
testFieldTree1 = Proxy

testFieldTree2 :: (d ~ (P (P [Char] Char) (P Char [Char])),
  FieldTree d ns,
  FilterLastEq "p1" ns ~ r) => Proxy r
testFieldTree2 = Proxy

testEq :: Proxy (P a b == String) -- ought to reduce
testEq = Proxy

type FilterLastEq n ns = FilterFstEq n (MapLast ns)

type family FilterFstEq n xs where
  FilterFstEq n ('(n,x) ': xs) = x ': FilterFstEq n xs
  FilterFstEq n (x ': xs) = FilterFstEq n xs
  FilterFstEq n '[] = '[]

type family MapLast (xs :: [[k]]) where
  MapLast (x ': xs) = '(Last x, x) ': MapLast xs
  MapLast '[] = '[]

type family Last (xs :: [k]) :: k where
  Last '[x] = x
  Last (x ': xs) = Last xs

type family MapSGP r v ns :: [(Constraint, [Symbol])] where 
  MapSGP r v '[] = '[]
  MapSGP r v (n ': ns) = '(SetGetPath n r v, n) ': MapSGP r v ns


class FieldList1 (r :: *) (v :: [Symbol]) (b :: Bool) | r -> v b

instance (false ~ False, '[] ~ r) => FieldList1 x r false


-- | list all paths to lookup fields in r,
-- where fields are listed as instances of SetGet and FieldList1
class FieldTree (r :: *) (v :: [[Symbol]]) | r -> v



instance (FieldList1 r ns b,
    MapFieldTree r ns b vs) => FieldTree r vs

class MapFieldTree (r :: *) (ns :: [Symbol]) (b :: Bool) (vs :: [[Symbol]]) | r ns b -> vs

instance MapSingleton ns vs => MapFieldTree r ns False vs

-- | MapSingleton x xs is like  xs = map (:[]) x
class MapSingleton (x :: [k]) (xs :: [[k]]) | x -> xs, xs -> x
instance MapSingleton '[] '[]
instance MapSingleton xs xs' => MapSingleton (x ': xs) ('[x] ': xs')


instance (MapFieldTree1 r n vs1,
      MapFieldTree r ns True vs2,        
      vs ~ AppendL vs1 vs2) => MapFieldTree r (n ': ns) True vs

instance MapFieldTree r '[] True '[]

class MapFieldTree1 (r :: *) (n :: Symbol) (vs :: [[Symbol]]) | r n -> vs

instance (SetGet n r s, FieldTree s vs1,
        MapCons n vs1 vs) => MapFieldTree1 r n vs

tryFieldTree :: FieldTree x r => x -> Proxy r
tryFieldTree _ = Proxy

-- | MapCons x xs xxs is like  xxs = map (x : ) xs
class MapCons (x :: k) (xs :: [[k]]) (xxs :: [[k]]) | x xs -> xxs
instance MapCons x '[] '[ '[x] ]
instance MapCons x b r => MapCons x (a ': b) ( (x ':  a) ': r)

type family AppendL (x :: [k]) (y :: [k]) :: [k]
type instance AppendL '[] y = y
type instance AppendL (x ': xs) y = x ': AppendL xs y