title: Haskell type arithmetic: how to access type-level list of lists
body: <p>I am working on a type-level representation for cell-based database models that features queries as Haskell-types. I got stuck when trying to extract values from a more complex query type.</p>
  
  <p>Let me first show you code that works:</p>
  
  <pre><code>-- a model with datapoints defined by a list of "aspects"
  -- every aspect has a "dimension" and a list of dimensional values
  type Model = Double  $|$ Aspect "currency" '["eur", "usd"]
                        |$ Aspect "flowtype" '["stock", "flow"]
                        |$ Nil
  
  -- extract the aspects from the query type
  class GetAspectsSingle a where
    getAspectsSingle :: Proxy a -&gt; [(Dimension, DimValue)]
  
  instance (KnownSymbol d, KnownSymbol v, GetAspectsSingle as)
        =&gt; GetAspectsSingle (Aspect d v |$ as) where
    getAspectsSingle _ = (symbolText (Proxy :: Proxy d),
                          symbolText (Proxy :: Proxy v))
                           : (getAspectsSingle (Proxy :: Proxy as))
  
  instance GetAspectsSingle Nil where
    getAspectsSingle _ = []
  
  -- a dummy for the execution of a type-safe query
  -- where CellTypeSingle is a type function that evaluates to the expected type
  save :: (MonadIO m, GetAspectsSingle q)
        =&gt; Proxy model -&gt; Proxy q -&gt; CellTypeSingle model q -&gt; m ()
  -- just print aspects instead of actual query
  save Proxy query _ = liftIO . print $ getAspectsSingle query
  
  -- an example query
  query :: Proxy (Aspect "currency" "eur" |$ Aspect "flowtype" "stock" |$ Nil)
  query = Proxy
  
  test :: IO ()
  test = save (Proxy :: Proxy Model) query 3.3
  </code></pre>
  
  <p>The key idea is that the type function <code>CellTypeSingle</code> evaluates to <code>Double</code> and thus the above code compiles, only if <code>3.3</code> is of type <code>Double</code>.</p>
  
  <p>I want to have queries that allow the selection of several values (of same type) like this:</p>
  
  <pre><code>query :: Proxy (Aspect "currency" '["eur", "usd"] |$ Aspect "flowtype" '["stock"] |$ Nil)
  query = Proxy
  </code></pre>
  
  <p>I managed to implement the corresponding type function <code>CellTypeList</code> that evaluates to <code>[Double]</code> in the above case. In order to get the aspects, however, I have to "explode" the query first. I.e. the above query becomes a list of queries.
  This is what I tried.</p>
  
  <pre><code>saveList :: (MonadIO m, GetAspectsList q)
           =&gt; Proxy model -&gt; Proxy q -&gt; CellTypeList model q -&gt; m ()
  -- just print aspects instead of actual query
  save Proxy query _ = liftIO . print $ getAspectsList query
  
  class GetAspectsList query where
    type GetAspectsListType (query :: Type) :: Type
    getAspectsList :: Proxy query -&gt; GetAspectsListType query -&gt; [[(Dimension, DimValue)]]
  
  instance (GetAspectsList as)
        =&gt; GetAspectsList (a |$ as) where
    type GetAspectsListType (a |$ as) = GetAspectsListType (ExplodeQuery (a |$ as))
    getAspectsList = ???
  </code></pre>
  
  <p>Now I got stuck: <code>ExplodeQuery</code> evaluates to <code>'[ '[ Aspect "currency" "eur", Aspect "flowtype" "stock" ], '[ Aspect "currency" "usd", Aspect "flowtype" "stock"] ]</code>, that is a list of lists on type-level.</p>
  
  <p>I don't know how to extract the <em>dimension</em> and <em>dimensional values</em> from there.</p>