[Haskell-cafe] using scoped type variables in proofs...

[Richard Eisenberg]

In my opinion, ScopedTypeVariables is rough around the edges. Here's what (I think) is going on:

In your problematic

>     (Refl :: (a :+ b1) :== (b1 :+ a)) ->

you are binding variable b1 in a pattern. This is an allowed feature of ScopedTypeVariables. The problem is that b1's only occurrence appears under a type function, so GHC is skittish about letting this be a *definition* for b1. (For example, we don't like defining a term level function like `foo (n + k) = n - k`! That would be utterly ambiguous.) So the type annotation is rejected.

But why, you ask, is this allowed a few lines previously? Here's the context:

> theoremPlusAbelian (SZ :: SNat a) ((SS a) :: SNat b) =
> -- forall 0 and a + 1
>   case theoremPlusAbelian (SZ :: SNat a) (a :: (b ~ 'S b1) => SNat b1) of
>     (Refl :: (a :+ b1) :== (b1 :+ a)) ->

This is accepted. But this is actually OK. We know that `a` is really `'Z` here. So, in the type annotation for `Refl`, GHC rewrites `a` with `'Z`. Then, it simplifies `'Z :+ b1` to `b1`. Aha! Now `b1` appears outside of a type function argument, so GHC is happy to use this as a definition. Note that such reasoning is not possible in the other case.

How to fix? We need to define (that is, bind) b1 elsewhere. The following works for me:

> theoremPlusAbelian ((SS a) :: (SNat a)) ((SS (b :: SNat b1)))      =
>   case theoremPlusAbelian ((SS a) :: (SNat a)) (b :: (b ~ 'S b1) => SNat b1) of
>     (Refl :: (a :+ b1) :== (b1 :+ a)) ->

Note that in the first line of this snippet, I bind `b1` in the type signature, not `b`. This isn't exactly beautiful because it lacks parallelism with the other cases, but I didn't see another way.

As an annoying corner case that you might stumble upon soon, when you say

> case foo of
>   (Blah :: some_type) -> ...

GHC will pretend you said

> case foo :: some_type of
>   Blah -> ...

but scope any variables in some_type over the right-hand side of the Blah pattern. This is probably not what you want, if Blah is a GADT type constructor that refines variables. This weird behavior extends to pattern-matches that match against an argument to a function. Note that this weird behavior is different to when you put a type annotation anywhere under the top-level of a pattern.

Richard

On May 11, 2015, at 6:33 AM, "Nicholls, Mark" <nicholls.mark at vimn.com> wrote:

> Hello,
>  
> I have written the below proof as an exercise.
>  
> I want to explicitly annotate the proof with type variables…..but I cant get a line to work…
>  
> > {-# LANGUAGE DataKinds #-}
> > {-# LANGUAGE ExplicitForAll #-}
> > {-# LANGUAGE FlexibleContexts #-}
> > {-# LANGUAGE FlexibleInstances #-}
> > {-# LANGUAGE GADTs #-}
> > {-# LANGUAGE MultiParamTypeClasses #-}
> > {-# LANGUAGE PolyKinds #-}
> > {-# LANGUAGE StandaloneDeriving #-}
> > {-# LANGUAGE TypeFamilies #-}
> > {-# LANGUAGE TypeOperators #-}
> > {-# LANGUAGE UndecidableInstances #-}
> > {-# LANGUAGE ScopedTypeVariables #-}
>  
> > import Prelude hiding (head, tail, (++), (+), replicate)
> > import qualified Prelude as P
>  
> > data Nat where
> >   Z :: Nat
> >   S :: Nat -> Nat
>  
> > data SNat (a :: Nat) where
> >   SZ :: SNat 'Z
> >   SS :: SNat a -> SNat ('S a)
>  
> here a nice plus
>  
> > type family   (n :: Nat) :+ (m :: Nat) :: Nat
> > type instance Z     :+ m = m
> > type instance (S n) :+ m = S (n :+ m)
>  
> lets try to do
>  
> > data val1 :== val2 where
> >   Refl :: val :== val
>  
> If I prove its abelian then we get it...
>  
> the "proof" works if we remove the type annotation
> but I want the annotation to convince myself I know whats going on.
>  
>  
> > theoremPlusAbelian :: SNat a -> SNat b -> (a :+ b) :== (b :+ a)
> > theoremPlusAbelian (SZ :: SNat a) (SZ :: SNat b) =
> > -- forall 0 and 0
> >   (Refl :: (a :+ b) :== (b :+ a))
> > theoremPlusAbelian ((SS a) :: SNat a) (SZ :: SNat b) =
> > -- forall a + 1 and 0
> >   case theoremPlusAbelian (a :: (a ~ 'S a1) => SNat a1) (SZ :: SNat b) of
> >     (Refl :: (a1 :+ b) :== (b :+ a1)) ->
> >       (Refl :: (a :+ b) :== (b :+ a))
> > theoremPlusAbelian (SZ :: SNat a) ((SS a) :: SNat b) =
> > -- forall 0 and a + 1
> >   case theoremPlusAbelian (SZ :: SNat a) (a :: (b ~ 'S b1) => SNat b1) of
> >     (Refl :: (a :+ b1) :== (b1 :+ a)) ->
> >       (Refl :: (a :+ b) :== (b :+ a))
> > -- cant seem to prove this...
> > theoremPlusAbelian ((SS a) :: (SNat a)) ((SS b) :: (SNat b))      =
> > -- forall a+1 and b+1
> > -- 1st prove (a + 1) + b =  b + (a + 1)...from above
> >   case theoremPlusAbelian ((SS a) :: (SNat a)) (b :: (b ~ 'S b1) => SNat b1) of
>  
> THE COMMENTED LINE FAILS.
>  
> Could not deduce ((b1 :+ 'S a1) ~ (a2 :+ 'S a1))
>     from the context (a ~ 'S a1)
>       bound by a pattern with constructor
>                  SS :: forall (a :: Nat). SNat a -> SNat ('S a),
>                in an equation for ‘theoremPlusAbelian’
>       at Cafe2.lhs:57:24-27
>     or from (b ~ 'S a2)
>       bound by a pattern with constructor
>                  SS :: forall (a :: Nat). SNat a -> SNat ('S a),
>                in an equation for ‘theoremPlusAbelian’
>       at Cafe2.lhs:57:45-48
>     NB: ‘:+’ is a type function, and may not be injective
>     The type variable ‘b1’ is ambiguous
>     Expected type: (a :+ a2) :== (a2 :+ a)
>       Actual type: (a :+ b1) :== (b1 :+ a)
>     Relevant bindings include
>       b :: SNat a2 (bound at Cafe2.lhs:57:48)
>       a :: SNat a1 (bound at Cafe2.lhs:57:27)
>     In the pattern: Refl :: (a :+ b1) :== (b1 :+ a)
>     In a case alternative:
>         (Refl :: (a :+ b1) :== (b1 :+ a))
>           -> case theoremPlusAbelian a (SS b) of {
>                Refl -> case theoremPlusAbelian a b of { Refl -> Refl } }
>     In the expression:
>       case
>           theoremPlusAbelian ((SS a) :: SNat a) (b :: b ~ S b1 => SNat b1)
>       of {
>         (Refl :: (a :+ b1) :== (b1 :+ a))
>           -> case theoremPlusAbelian a (SS b) of {
>                Refl -> case theoremPlusAbelian a b of { Refl -> ... } } }
>  
>  
>  
> >     -- (Refl :: (a :+ b1) :== (b1 :+ a)) ->
> >     Refl ->
> > -- now prove a + (b + 1) =  (b + 1) + a...from above
> >       case theoremPlusAbelian a (SS b) of
> >         Refl ->
> > -- now prove a + b = b + a
> >           case theoremPlusAbelian a b of
> > -- which seems to have proved a + b = b + a
> >             Refl -> Refl
>  

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20150511/2de38cec/attachment-0001.html>