Singletons in Heterogenous Lists

Question

Я хотел бы написать функцию, которая анализирует гетерогенный список. Ради аргумента, давайте следующему

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

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

Конечной целью была бы написать что-то вроде следующих

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 

Характерных бит в том, что analyzeRec использует знание ограничений экземпляров на каждый тип и значение в Rec. Этот основанный на классе механизм работает, но неуклюж и многословен в случае, когда вы должны делать это снова и снова (и я это делаю).

Итак, я бы предпочел вместо этого заменить этот механизм на singletons. Вместо этого я хотел бы написать такую ​​функцию, как

-- 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 

, но это, очевидно, падает ровно, по крайней мере, в нескольких измерениях.

Что такое «правильный» способ записи такой функции по гетерогенным спискам с использованием техники Singletons? Есть ли лучший способ подойти к этой проблеме? Что я должен ожидать в решении такого рода вещей?

(Для справки, это для экспериментального Слуга клона под названием Serv. Соответствующие файлы Serv.Internal.Header.Serialization и Serv.Internal.Header в качестве фона. Я хотел бы написать функцию, которая принимает в гетерогенном списке помеченных значений заголовка, а затем headerEncode их в список фактических (ByteString, ByteString) пар.)

Answer 1

Я попытаюсь представить здесь в «идиоматическое» singletons решение (если такое вообще существует). Отборочные:

{-# 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 

Нам нужно All c rs ограничения, но мы даем ему спину и сделать cTyFun вместо простого a -> Constraint конструктора:

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

TyFun позволяет нам абстрактный над конструкторами типа и типа семьи и дает нам частичное применение. Это дает нам почти первоклассные функции уровня типа с несколько уродливым синтаксисом. Обратите внимание, что мы обязательно теряем конструкторскую инъективность. @@ является оператором по применению TyFun-s. TyFun a b -> * означает, что a - это вход, а b - это выход, а конечный -> * - это просто артефакт кодирования. С GHC 8.0 мы сможем только сделать

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

И использовать a ~> b в дальнейшем.

Мы можем реализовать теперь общую «классное» отображение над 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 

Обратите внимание, что выше c имеет вид TyFun (a, *) Constraint -> *.

А затем реализовать 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)) 

Во-первых, c ~ UncurrySym1 (TyCon2 Analyze) это просто уровень типа let связывания, что позволяет мне использовать c в Proxy c как стенографии. (Если бы я действительно хотел использовать все грязные трюки, я бы добавил {-# LANGUAGE PartialTypeSignatures #-} и напишу Proxy :: _ c).

UncurrySym1 (TyCon2 Analyze) делает то же самое, что и uncurry Analyze, если бы у Haskell была полная поддержка функций уровня. Очевидным преимуществом здесь является то, что мы можем выписать тип analyzeRec на лету без дополнительных семейств или классов типа верхнего уровня, а также использовать AllC в более общем плане.

---

В качестве бонуса, давайте удалить SingI ограничение из Analyze, и попытаться осуществить analyzeRec.

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

Теперь мы должны требовать дополнительное ограничение, которое выражает, что все name -s в нашем Rec являются SingI.Мы можем использовать два cMapRec -s и заархивировать результаты:

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) 

TyCon1 SingI :.$$$ FstSym0 Здесь можно перевести как SingI . fst.

Это все еще примерно в пределах уровня абстракции, который может быть легко выражено с TyFun -s. Главным ограничением, конечно же, является отсутствие лямбда. В идеале нам не нужно было бы использовать zip, вместо этого мы использовали бы AllC (\(name, t) -> (SingI name, Analyze name t)) и использовали один cMapRec. С singletons, если мы не сможем использовать крыло с беспроблемным программированием на уровне шрифта, мы должны ввести новое точечное семейство типов.

Занятно, GHC 8,0 будет достаточно сильным, чтобы мы могли реализовать лямбды типа уровня с нуля, хотя это будет, наверное, некрасиво, как ад. Например, \p -> (SingI (fst p), uncurry Analyze p) может выглядеть примерно так:

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

где все L postfixes обозначают термин лямбда вложения обычных TyFun -s (пока другой коллекции будет сокращения от порожденную TH ...).

У меня есть prototype, хотя он работает только с еще более уродливыми переменными de Bruijn, из-за ошибки GHC. В нем также есть Fix и явная лень на уровне типа.

Answer 2

Я думаю, что это звуковой подход, это просто так. Иногда вам нужно немного помочь системе типов.

Во-первых, то, как вы пишете предикат All, имеет большое значение (если оно уменьшается в надлежащее время), и я не знаю, какой из All вы используете.

Кроме того, вы используете symbolVal на имя, но нет никаких доказательств того, что это KnownSymbol - вы должны добавить этот документ где-нибудь. Единственное очевидное место, мне, на классе типа:

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

Вот является All предикат:

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

Обратите внимание, что эта линия

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

не тип проверки (это не очень хорошо). Каждый элемент rs является кортежем. Мы могли бы написать All' :: (k0 -> k1 -> Constraint) -> [(k0,k1)] -> Constraint непосредственно так же, как All'. Но funner написать типа класса 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) 

Если это Uncurry выглядит чрезвычайно сложной, это опять-таки, потому что это важно для Uncurry c '(x,y), чтобы свести к c x y в нужное время, так написано в пути что (или, вернее, позволяет) методу typechecker уменьшить это ограничение всякий раз, когда он его видит.Теперь функция

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 

Это не использует ничего из singletons и не нужно.

---

Полный рабочий код

{-# 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