Weitere Probleme mit abhängig typisierte Programmierung in Haskell

Question

Ich arbeite in einem Beispiel für abhängig typisierte Programm in Haskell und ich möchte einen Beweis der propositional Gleichheit Typ a :~: b definiert in singletons Bibliothek "umschreiben".

Genauer gesagt, ich habe einen Datentyp für den Nachweis der Mitgliedschaft in regulären Ausdrücken. Mein Problem ist, wie man sich mit dem Beweis der Verkettung zweier regulärer Ausdrücke beschäftigt. In meinem Code habe ich eine GADT namens InRegExp xs e, die die Tatsache ausdrückt, dass xs in der Sprache des regulären Ausdrucks e ist. Für die Verkettung habe ich folgenden Konstruktor:

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

So weit, so gut. Jetzt mag ich eine Umkehrung Lemma für die Mitgliedschaft in Verkettung von zwei regulären Ausdrücken definieren:

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

aber der Code wird von GHC mit folgenden Fehlermeldung abgewiesen:

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

In Agda oder Idris, diese Art der Inversion Lemma funktioniert gut. Ist es möglich, ein solches Inversionslemma in Haskell auszudrücken? Der vollständige Code ist im folgenden gist verfügbar.

Jeder Tipp oder eine Erklärung, wie ich ein solches Lemma ausdrücken kann oder warum es nicht möglich ist, es auszudrücken, wird sehr geschätzt.

Answer 1

Die einfachste Methode zum Schreiben von abhängig typisierten Programmen in Haskell besteht darin, zuerst in Agda zu schreiben, dann durch Sing x -> b zu ersetzen. Wir können jedoch Proxy anstelle von Sing verwenden, wenn wir sicher sind, dass wir keine Werte berechnen müssen.

In unserem Fall (unser Ziel, unter der Annahme, hasEmpty von Ihrem Kern zu schreiben), brauchen wir nur eine einzige Sing im Cat Konstruktor, weil wir mit einem Muster übereinstimmen Beweis für die folgende Funktion benötigen:

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 stellt fest, dass die Unterlisten der leeren Liste auch leer sind, so dass wir sie im Cat Fall für hasEmpty verwenden können. Wie auch immer, unten ist der ganze Code.

Ich verwendete eine etwas andere, aber äquivalente Definition für Star, die Choice und Eps für den Aufbau einer Listenstruktur wiederverwendet.

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