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

[Roman Cheplyaka]

Actually, I was wrong there.

The paper "Lexically-scoped type variables" from 2004 claims that
variables only get bound in value bindings, but GHC has changed its
design since.

The docs say expression signatures do bind type variables:
http://bit.ly/1GZ7VQw

On 11/05/15 15:43, Nicholls, Mark wrote:
> That worked!....
> 
> But doesn’t seem to be true of all the previous cases!
> 
> i.e.
> 
> The b1 here is bound quite happily
> 
>> 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))
> 
> yet
> 
>> 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
>>      (Refl :: (a :+ b1) :== (b1 :+ a)) -> 
> 
> Complains
> 
> There seems little difference?
> 
> 
>> GHC tells you that b1 is ambiguous, so that should tell you that it isn't getting
>> bound in the case expression as you'd think.
>>
>> The reason is that type variables only get bound at value bindings; but you
>> attached the signature to an expression.
>>
>> To fix it, move the annotation to the pattern like this:
>>
>> theoremPlusAbelian ((SS a) :: (SNat a)) ((SS (b :: SNat b1)) :: (SNat b)) =
>>
>>
>> On 11/05/15 13:33, Nicholls, Mark 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
>>>
>>>
>>>
>>>
>>>
>>>
>>>
>>>
>>>
>>> CONFIDENTIALITY NOTICE
>>>
>>> This e-mail (and any attached files) is confidential and protected by
>>> copyright (and other intellectual property rights). If you are not the
>>> intended recipient please e-mail the sender and then delete the email
>>> and any attached files immediately. Any further use or dissemination
>>> is prohibited.
>>>
>>> While MTV Networks Europe has taken steps to ensure that this email
>>> and any attachments are virus free, it is your responsibility to
>>> ensure that this message and any attachments are virus free and do not
>>> affect your systems / data.
>>>
>>> Communicating by email is not 100% secure and carries risks such as
>>> delay, data corruption, non-delivery, wrongful interception and
>>> unauthorised amendment. If you communicate with us by e-mail, you
>>> acknowledge and assume these risks, and you agree to take appropriate
>>> measures to minimise these risks when e-mailing us.
>>>
>>> MTV Networks International, MTV Networks UK & Ireland, Greenhouse,
>>> Nickelodeon Viacom Consumer Products, VBSi, Viacom Brand Solutions
>>> International, Be Viacom, Viacom International Media Networks and VIMN
>>> and Comedy Central are all trading names of MTV Networks Europe.  MTV
>>> Networks Europe is a partnership between MTV Networks Europe Inc. and
>>> Viacom Networks Europe Inc.  Address for service in Great Britain is
>>> 17-29 Hawley Crescent, London, NW1 8TT.
>>>
>>>
>>>
>>> _______________________________________________
>>> Haskell-Cafe mailing list
>>> Haskell-Cafe at haskell.org
>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20150511/291db760/attachment.sig>