Haskell中的依賴類型編程的更多問題

Question

我正在處理Haskell中的依賴類型程序的一個示例，我想「重寫」一個在singletons庫中定義的命題相等類型a :~: b的證據。

更具體地說，我有一個數據類型來表示正則表達式成員的證據。我的麻煩是如何處理兩個正則表達式串聯的證據。在我的代碼中，我有一個名爲InRegExp xs e的GADT，它表示xs是使用正則表達式e的語言。對於級聯，我有以下構造函數：

InCat :: InRegExp xs l -> InRegExp ys r -> 
     (zs :~: xs ++ ys) -> InRegExp zs (Cat l r) 

到目前爲止，這麼好。現在，我想在兩個正則表達式的串聯來定義反轉引理成員：

inCatInv :: InRegExp (xs ++ ys) (Cat e e') -> (InRegExp xs e , InRegExp ys e') 
inCatInv (InCat p p' Refl) = (p , p') 

但是代碼是由GHC與以下錯誤消息拒絕：

Could not deduce (xs1 ~ xs) 
    from the context ('Cat e e' ~ 'Cat l r) 
     bound by a pattern with constructor 
      InCat :: forall (zs :: [Nat]) 
          (xs :: [Nat]) 
          (l :: RegExp [Nat]) 
          (ys :: [Nat]) 
          (r :: RegExp [Nat]). 
         InRegExp xs l 
         -> InRegExp ys r -> zs :~: (xs ++ ys) -> InRegExp zs ('Cat l r), 
      in an equation for ‘inCatInv’ 
    at /Users/rodrigo/Dropbox/projects/haskell/experiments/src/Lib.hs:44:11-25 
or from ((xs ++ ys) ~ (xs1 ++ ys1)) 
    bound by a pattern with constructor 
      Refl :: forall (k :: BOX) (b :: k). b :~: b, 
      in an equation for ‘inCatInv’ 
    at /Users/rodrigo/Dropbox/projects/haskell/experiments/src/Lib.hs:44:22-25 
    ‘xs1’ is a rigid type variable bound by 
     a pattern with constructor 
      InCat :: forall (zs :: [Nat]) 
          (xs :: [Nat]) 
          (l :: RegExp [Nat]) 
          (ys :: [Nat]) 
          (r :: RegExp [Nat]). 
        InRegExp xs l 
        -> InRegExp ys r -> zs :~: (xs ++ ys) -> InRegExp zs ('Cat l r), 
     in an equation for ‘inCatInv’ 
     at /Users/rodrigo/Dropbox/projects/haskell/experiments/src/Lib.hs:44:11 
    ‘xs’ is a rigid type variable bound by 
     the type signature for 
     inCatInv :: InRegExp (xs ++ ys) ('Cat e e') 
        -> (InRegExp xs e, InRegExp ys e') 
     at /Users/rodrigo/Dropbox/projects/haskell/experiments/src/Lib.hs:43:13 
Expected type: InRegExp xs e 
    Actual type: InRegExp xs1 l 
Relevant bindings include 
    p :: InRegExp xs1 l 
    (bound at /Users/rodrigo/Dropbox/projects/haskell/experiments/src/Lib.hs:44:17) 
    inCatInv :: InRegExp (xs ++ ys) ('Cat e e') 
       -> (InRegExp xs e, InRegExp ys e') 
    (bound at /Users/rodrigo/Dropbox/projects/haskell/experiments/src/Lib.hs:44:1) 
In the expression: p 
In the expression: (p, p') 

在阿格達或伊德里斯，這反轉引理類型很好。在Haskell中可以表達這樣的反轉引理嗎？完整的代碼可在以下gist中找到。

任何提示或解釋我如何表達這樣的引理或爲什麼它是不可能表達的高度讚賞。

Answer 1

在Haskell中編寫依賴類型程序最簡單的方法是先寫入Agda，然後用Sing x -> b替換(x : A) -> B。但是，我們可以使用Proxy而不是Sing，因爲我們確信我們不需要使用值進行計算。

在我們的情況下（假設我們的目標是從你的要點寫hasEmpty），我們只需要在Cat構造一個Sing，因爲我們需要匹配以下功能證明一個規律：

appendEmpty :: Sing xs -> Proxy ys -> (xs :++ ys) :~: '[] -> (xs :~: '[], ys :~: '[]) 
appendEmpty SNil   ys eq = (Refl, eq) 
appendEmpty (SCons x xs) ys eq = case eq of {} 

appendEmpty確定空列表的子列表也是空的，所以我們可以在的情況下使用hasEmpty。無論如何，下面是整個代碼。

我對Star使用了稍微不同但等效的定義，它們重用Choice和Eps來構建列表結構。

{-# language 
    TemplateHaskell, UndecidableInstances, LambdaCase, EmptyCase, 
    DataKinds, PolyKinds, GADTs, TypeFamilies, ScopedTypeVariables, 
    TypeOperators #-} 

import Data.Singletons.Prelude 
import Data.Singletons.TH 
import Data.Proxy 

$(singletons [d| 
    data Regex c 
    = Sym c 
    | Cat (Regex c) (Regex c) 
    | Choice (Regex c) (Regex c) 
    | Star (Regex c) 
    | Eps 
    deriving (Show) 
|]) 

appendEmpty :: Sing xs -> Proxy ys -> (xs :++ ys) :~: '[] -> (xs :~: '[], ys :~: '[]) 
appendEmpty SNil   ys eq = (Refl, eq) 
appendEmpty (SCons x xs) ys eq = case eq of {} 

data InRegex :: [c] -> Regex c -> * where 
    InEps :: InRegex '[] Eps 
    InSym :: InRegex '[c] (Sym c) 
    InCat :: Sing xs -> InRegex xs l -> InRegex ys r -> InRegex (xs :++ ys) (Cat l r) 
    InLeft :: InRegex xs l -> InRegex xs (Choice l r) 
    InRight :: InRegex ys r -> InRegex ys (Choice l r) 
    InStar :: InRegex xs (Choice Eps (Cat r (Star r))) -> InRegex xs (Star r) 

hasEmpty :: Sing r -> Either (InRegex '[] r) (InRegex '[] r -> Void) 
hasEmpty (SSym _) = Right (\case {}) 
hasEmpty (SCat l r) = case hasEmpty l of 
    Left inl -> case hasEmpty r of 
    Left inr -> Left (InCat SNil inl inr) 
    Right notInr -> Right 
     (\(InCat xs inl (inr :: InRegex ys r)) -> case appendEmpty xs (Proxy :: Proxy ys) Refl of 
      (Refl, Refl) -> notInr inr) 
    Right notInl -> Right 
    (\(InCat xs inl (inr :: InRegex ys r)) -> case appendEmpty xs (Proxy :: Proxy ys) Refl of 
     (Refl, Refl) -> notInl inl) 
hasEmpty (SChoice l r) = case hasEmpty l of 
    Left inl  -> Left (InLeft inl) 
    Right notInl -> case hasEmpty r of 
    Left inr  -> Left (InRight inr) 
    Right notInr -> Right (\case 
     InLeft inl -> notInl inl 
     InRight inr -> notInr inr) 
hasEmpty (SStar r) = Left (InStar (InLeft InEps)) 
hasEmpty SEps = Left InEps