Haskellで依存型プログラミングの問題

Question

私はHaskellの依存型プログラムの例で作業していますが、という定義命題型の証拠をsingletonsライブラリに定義して "書き直したい"と思います。

具体的には、正規表現メンバーシップの証拠を表すデータ型があります。私の問題は、2つの正規表現を連結した証拠をどう扱うかです。私のコードではInRegExp xs eと呼ばれるGADTを持っていて、xsは正規表現の言語であるeであることを表しています。連結のために、私は次のコンストラクタを持っています：

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

これまでのところ、とても良いです。今私は2つの正規表現の連結のメンバーシップのために反転補題を定義したい：

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

が、コードは、次のエラーメッセージでGHCによって拒否された：Agdaまたはイドリスで

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

、この一種の反転補助定理はうまく動作します。ハスケルでそのような補題を表現することは可能ですか？完全コードは、gistで利用可能です。

このような補題をどのように表現することができるのか、それが表現できないのかについてのヒントや説明は高く評価されます。

Answer 1

ハスケルで依存型プログラムを書く最も簡単な方法は、最初にAgdaに書き込んでから、(x : A) -> BをSing x -> bに置き換えます。ただし、値を計算する必要がない場合は、Singの代わりにProxyを使用できます。我々の場合には

（私たちの目標は、あなたの主旨から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は、空リストのサブリストも空であることを確認しているので、CatのケースではhasEmptyに使用することができます。とにかく、以下は全体のコードです。

リスト構造を構築するためにChoiceとEpsを再利用しているStarについては少し異なるが、同等の定義を使用しました。

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