Singletons in Heterogenous Lists

Question

I'd like to write a function which analyzes a heterogenous list. For sake of argument, let's have the following

data Rec rs where
  Nil :: Rec '[]
  Cons :: ty -> Rec rs -> Rec ( '(name, ty) ': rs )

class Analyze name ty where
  analyze :: Proxy name -> ty -> Int

The ultimate goal would be to write something like the following

class AnalyzeRec rs where
  analyzeRec :: Rec rs -> [(String, Int)]

instance AnalyzeRec '[] where
  analyzeRec Nil = []

instance (Analyze name ty, AnalyzeRec rs) => 
           AnalyzeRec ( '(name, ty) ': rs ) 
  where
    analyzeRec (Cons hd tl) = 
      let proxy = Proxy :: Proxy name
      in (symbolVal proxy, analyze proxy hd) : analyzeRec tl

The salient bits being that analyzeRec uses knowledge of constraints instantiated at each type and value in the Rec. This class-based mechanism works, but is clunky and verbose in the case where you have to do this over and over (and I do).

So, I'd like to instead replace this with a singletons-based mechanism. I'd like to write instead a function like

-- no type class!
analyzeRec :: All Analyze rs => Rec rs -> [(String, Int)]
analyzeRec rec = 
  case rec of
    Nil -> []
    Cons hd tl -> withSing $ \s -> 
      (symbolVal s, analyze s hd) : analyzeRec tl

but this clearly falls flat in at least a few dimensions.

What is the "right" way to write such a function over heterogenous lists using the Singletons technique? Is there a better way to approach this problem? What should I expect in solving this sort of thing?

(For reference, this is for an experimental Servant clone called Serv. The relevant files are Serv.Internal.Header.Serialization and Serv.Internal.Header as background. I'd like to write a function which takes in a heterogenous list of tagged header values and then headerEncode them into a list of actual (ByteString, ByteString) pairs.)

Johnnyjumpup

Answer 1

I'll try to present here an "idiomatic" singletons solution (if such a thing even exists). Preliminaries:

{-# LANGUAGE
  RankNTypes, DataKinds, PolyKinds, ConstraintKinds, GADTs,
  TypeOperators, MultiParamTypeClasses, TypeFamilies, ScopedTypeVariables #-}

import Data.Singletons.Prelude
import Data.Proxy
import GHC.Exts (Constraint) 

-- SingI constraint here for simplicity's sake
class SingI name => Analyze (name :: Symbol) ty where
  analyze :: Proxy name -> ty -> Int

data Rec rs where
  Nil :: Rec '[]
  Cons :: ty -> Rec rs -> Rec ( '(name, ty) ': rs )

recName :: Rec ('(name, t) ': rs) -> Proxy name
recName _ = Proxy

We need an All c rs constraint, but we give it a spin and make c a TyFun instead a plain a -> Constraint constructor:

type family AllC (c :: TyFun a Constraint -> *) (rs :: [a]) :: Constraint where
  AllC c '[]       = ()
  AllC c (x ': xs) = (c @@ x, AllC c xs)

TyFun lets us abstract over type constructors and type families and gives us partial application. It gives us almost first-class type-level functions with a somewhat ugly syntax. Note though that we necessarily lose constructor injectivity. @@ is the operator for applying TyFun-s. TyFun a b -> * means that a is the input and b is the output, and the trailing -> * is just an artifact of the encoding. With GHC 8.0 we'll be able to just do

type a ~> b = TyFun a b -> *

And use a ~> b thereafter.

We can implement now a general "classy" mapping over Rec:

cMapRec ::
  forall c rs r.
  AllC c rs => Proxy c -> (forall name t. (c @@ '(name, t)) => Proxy name -> t -> r) -> Rec rs -> [r]
cMapRec p f Nil           = []
cMapRec p f r@(Cons x xs) = f (recName r) x : cMapRec p f xs

Note that above c has kind TyFun (a, *) Constraint -> *.

And then implement analyzeRec:

analyzeRec :: 
  forall c rs. (c ~ UncurrySym1 (TyCon2 Analyze)) 
  => AllC c rs => Rec rs -> [(String, Int)]
analyzeRec = cMapRec (Proxy :: Proxy c) (\p t -> (fromSing $ singByProxy p, analyze p t))

First, c ~ UncurrySym1 (TyCon2 Analyze) is just a type-level let binding that lets me use c in Proxy c as a shorthand. (If I really wanted to use all the dirty tricks, I would add {-# LANGUAGE PartialTypeSignatures #-} and write Proxy :: _ c).

UncurrySym1 (TyCon2 Analyze) does the same thing that uncurry Analyze would do if Haskell had full support for type level functions. The obvious advantage here is that we can write out the type of analyzeRec on the fly without extra top-level type families or classes, and also use AllC far more generally.

---

As a bonus, let's remove the SingI constraint from Analyze, and try to implement analyzeRec.

class Analyze (name :: Symbol) ty where
  analyze :: Proxy name -> ty -> Int

Now we have to require an additional constraint that expresses that all the name-s in our Rec are SingI. We can use two cMapRec-s, and zip the results:

analyzeRec ::
  forall analyze names rs.  
  (analyze ~ UncurrySym1 (TyCon2 Analyze),
   names   ~ (TyCon1 SingI :.$$$ FstSym0),
   AllC analyze rs,
   AllC names rs)
  => Rec rs -> [(String, Int)]
analyzeRec rc = zip
  (cMapRec (Proxy :: Proxy names)   (\p _ -> fromSing $ singByProxy p) rc)
  (cMapRec (Proxy :: Proxy analyze) (\p t -> analyze p t) rc)

Here TyCon1 SingI :.$$$ FstSym0 can be translated as SingI . fst.

This is still roughly within the level of abstraction that can be readily expressed with TyFun-s. The main limitation, of course, is the lack of lambdas. Ideally we wouldn't have to use zip, instead we would use AllC (\(name, t) -> (SingI name, Analyze name t)), and use a single cMapRec. With singletons, if we can't wing it anymore with point-free type-level programming, we have to introduce a new pointful type family.

Amusingly, GHC 8.0 will be strong enough so that we can implement type-level lambdas from scratch, although it will be probably ugly as hell. For example, \p -> (SingI (fst p), uncurry Analyze p) could look something like this:

Eval (
  Lam "p" $
    PairL :@@
      (LCon1 SingI :@@ (FstL :@@ Var "p")) :@@    
      (UncurryL :@@ LCon2 Analyze :@@ Var "p"))

where all the L postfixes denote the lambda term embeddings of ordinary TyFun-s (yet another collection of shorthands to be generated by TH...).

I have a prototype, although it only works with the even uglier de Bruijn variables yet, because of a GHC bug. It also features Fix and explicit laziness on the type level.

Chalcocite

Awesome! I had just figured out something like AllC and had been stuck on understanding the function symbols. I think I can make this work. I feel like going the full cMap route is too far at the moment, but it's close to feasible! – Johnnyjumpup

Feel free to ask about TyFun-s. They do involve a lot of syntactic noise, and it's likely worth an exposition. Also, you could look at this, if you haven't read it already. – Kneeland

I skimmed that post a while back but I think now I have the background to better understand it, thanks again for the reference! – Johnnyjumpup

Here are some attempts to wedge this into my code: github.com/tel/serv/blob/feat-singletons/src/Serv/Internal/… github.com/tel/serv/blob/feat-singletons/src/Serv/Internal/… and github.com/tel/serv/blob/feat-singletons/src/Serv/Internal/…. I'll want to get confident with these techniques before diving into Server.hs. – Johnnyjumpup

Answer 2

I think this is a sound approach, it's just that .. sometimes you need to help the type system out a bit.

Firstly, the way you write the All predicate matters a lot (if it reduces at the proper times) and I don't know which All you are using.

Also, you are using symbolVal on the name but there is no proof that it is a KnownSymbol - you must add this proof somewhere. The only obvious place, to me, is on the type class:

class KnownSymbol name => Analyze name ty where
  analyze :: Proxy name -> ty -> Int

Here is the All predicate:

type family All (c :: k -> Constraint) (xs :: [k]) :: Constraint where 
  All c '[] = () 
  All c (x ': xs) = (c x, All c xs) 

Note that this line

analyzeRec :: All Analyze rs => Rec rs -> [(String, Int)]

does not type check (it is not well kinded). Each element of rs is a tuple. We could write All' :: (k0 -> k1 -> Constraint) -> [(k0,k1)] -> Constraint directly much in the same way as All'. But it is funner to write a type class Uncurry:

type family Fst (x :: (k0, k1)) :: k0 where 
  Fst '(x,y) = x 

type family Snd (x :: (k0, k1)) :: k1 where 
  Snd '(x,y) = y 

class (c (Fst x) (Snd x)) => Uncurry (c :: k0 -> k1 -> Constraint) (x :: (k0, k1)) where 
instance (c x y) => Uncurry c '(x, y)

If this Uncurry looks exceedingly complicated, it is again because it is important for Uncurry c '(x,y) to reduce to c x y at the right time, so it is written in a way that forces (or rather allows) the typechecker to reduce this constraint whenever it sees it. Now the function is

analyzeRec :: All (Uncurry Analyze) rs => Rec rs -> [(String, Int)]
analyzeRec r = 
  case r of
    Nil -> []
    (Cons hd tl) -> let s = recName r in (symbolVal s, analyze s hd) : analyzeRec tl

-- Helper
recName :: Rec ('(name,ty)':rs) -> Proxy name 
recName _ = Proxy 

This doesn't use anything from singletons nor does it need it.

---

Complete working code

{-# LANGUAGE PolyKinds, ConstraintKinds, UndecidableInstances, TypeOperators #-}
{-# LANGUAGE DataKinds, GADTs, MultiParamTypeClasses, TypeFamilies, FlexibleInstances, FlexibleContexts #-} 

import Data.Proxy 
import GHC.TypeLits 
import GHC.Prim (Constraint)

data Rec rs where
  Nil :: Rec '[]
  Cons :: ty -> Rec rs -> Rec ( '(name, ty) ': rs )

class KnownSymbol name => Analyze name ty where
  analyze :: Proxy name -> ty -> Int

type family All (c :: k -> Constraint) (xs :: [k]) :: Constraint where 
  All c '[] = () 
  All c (x ': xs) = (c x, All c xs) 

type family Fst (x :: (k0, k1)) :: k0 where 
  Fst '(x,y) = x 

type family Snd (x :: (k0, k1)) :: k1 where 
  Snd '(x,y) = y 

class (c (Fst x) (Snd x)) => Uncurry (c :: k0 -> k1 -> Constraint) (x :: (k0, k1)) where 
instance (c x y) => Uncurry c '(x, y)

recName :: Rec ('(name,ty)':rs) -> Proxy name 
recName _ = Proxy 

analyzeRec :: All (Uncurry Analyze) rs => Rec rs -> [(String, Int)]
analyzeRec r = 
  case r of
    Nil -> []
    (Cons hd tl) -> let s = recName r in (symbolVal s, analyze s hd) : analyzeRec tl

Gader

Huh, I thought I tried this in the past and it broke down. I'll try following your code example closely, now. Thanks! – Johnnyjumpup

@dfeuer class (...) => Uncurry c '(x, y) is simply not a valid class declaration.. and instance (c (Fst x) (Snd x)) => Uncurry c x is perfectly valid and the code works just the same.. the other version is just less characters to type. – Gader

Oh, right, silly me. So the obvious way, I suppose, is class (c p q, x ~ '(p, q)) => Uncurry c x. Is that problematic? – Esophagus

No because that also isn't a valid class declaration, all the variables in the left hand side must appear in the right hand side. – Gader