More problems with dependently typed programming in Haskell

Question

I'm working in an example of dependently typed program in Haskell and I would like to "rewrite" an evidence of propositional equality type a :~: b defined in singletons library.

More specifically, I have a data type for represent evidence of regular expression membership. My trouble is how to deal with evidence of concatenation of two regular expressions. In my code, I have a GADT called InRegExp xs e that express the fact that xs is in the language of regular expression e. For concatenation, I have the following constructor:

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

So far, so good. Now I want to define an inversion lemma for membership in concatenation of two regular expressions:

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

but the code is rejected by GHC with the following error message:

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 or Idris, this kind of inversion lemma works just fine. Is possible to express such inversion lemma in Haskell? The complete code is available in the following gist.

Any tip or explanation of how can I express such lemma or why it isn't possible to express is highly appreciated.

The problem you are having is non-injective type families. Unfortunately there is no real easy way around this. Essentially you have (xs ++ ys) ~ (xs' ++ ys') - remember that the xs and ys inside the constructor are existentially quantified, so they give rise to new type variables - from which the compiler is unable to deduce that xs ~ xs' and ys ~ ys'. Instead of using propositional equality, you'll need to have an inductive proof that xs ++ ys = zs - I'm guessing that inCatInv will have to be recursive as well. — user2407038
This looks fundamentally impossible: at the type level, [] ++ [x] is indistinguishable from [x] ++ [], and so the type of inCatInv is inherently ambiguous. More precisely, whoever calls inCatInv gets to choose xs,ys, with the only constraint that xs++ys is the same list as in the InRegExp type. So, the inCatInv type is promising to the caller that it can split zs into any possible way as xs++ys (caller's choice), which is not what it really does (nor what it is intended to do, AFAICS). — chi
Your lemma doesn't seem true. InRegexp ("ab" ++ "c") (Cat "a" "bc") doesn't imply InRegexp "ab" "a". — András Kovács
@user2407038: In order to have an inductive proof of xs ++ ys = zs, I'll need to recurse over the structure of xs, using a singleton SList xs, right? Or there's other way to do this? — Rodrigo Ribeiro
@RodrigoRibeiro Yes, that is correct - you'll need a list singleton. You could of course postulate that it is correct with unsafeCoerce which would not required a SList (just a Proxy). — user2407038

András Kovács András Kovács · Accepted Answer · 2016-04-15T22:03:04

The simplest method for writing dependently typed programs in Haskell is to first write it in Agda, then replace (x : A) -> B with Sing x -> b. However, we can use Proxy instead of Sing when we're sure we won't need to compute with values.

In our case (assuming our goal is to write hasEmpty from your gist), we only need a single Sing in the Cat constructor, because we need a pattern matching proof for the following function:

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 establishes that the sublists of the empty list are empty too, so we can use them in the Cat case for hasEmpty. Anyway, below's the whole code.

I used a slightly different but equivalent definition for Star that reuses Choice and Eps for building a list structure.

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

More problems with dependently typed programming in Haskell

1 Answers