[Haskell-cafe] using scoped type variables in proofs...
Roman Cheplyaka
roma at ro-che.info
Mon May 11 17:34:39 UTC 2015
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>
More information about the Haskell-Cafe
mailing list