-
Notifications
You must be signed in to change notification settings - Fork 5
Part2_Sec8_1_eqproof
rpeszek edited this page Nov 20, 2018
·
3 revisions
Markdown generated from:
Source idr program: /src/Part2/Sec8_1_eqproof.idr
Source lhs program: /src/Part2/Sec8_1_eqproof.lhs
Dependent types are so rich that the type checker needs help in figuring things out. A proof of equality between natural numbers is needed to implement
exactLength : (len : Nat) -> (input : Vect m a) -> Maybe (Vect len a)
that, basically, checks if m is len and returns the vector if it is.
The following code matches section 8.1 in the book.
exactLength is reimplemented in Part2_Sec8_3_deceq using the DecEq interface.
module Part2.Sec8_1_eqproof
import Data.Vect
%default total
{-
Returns proof that num1 and num2 are equal
data (=) : a -> b -> Type where
Refl : x = x
cong : {func : a -> b} -> x = y -> func x = func y
-}
checkEqNat : (num1 : Nat) -> (num2 : Nat) -> Maybe (num1 = num2)
checkEqNat Z Z = Just Refl
checkEqNat Z (S k) = Nothing
checkEqNat (S k) Z = Nothing
checkEqNat (S k) (S j) = case checkEqNat k j of
Nothing => Nothing
Just prf => Just (cong prf)
{-
Notes: if the last line in defintion of exactLength is changed to
Just prf => ?hole
idris repl:
*Part2/Sec8_1_eqproof> :t hole
a : Type
m : Nat
len : Nat
prf : len = m
input : Vect m a
--------------------------------------
hole : Maybe (Vect len a)
When last line is replaced with:
Just prf => Just input
causes compiler error:
./Part2/Sec8_1_eqproof.idr:34:49-58:
|
34 | Just prf => Just input
| ~~~~~~~~~~
When checking right hand side of Part2.Sec8_1_eqproof.case block in exactLength at ./Part2/Sec8_1_eqproof.idr:32:14-29 with expected type
Maybe (Vect len a)
When checking argument x to constructor Prelude.Maybe.Just:
Type mismatch between
Vect m a (Type of input)
and
Vect len a (Expected type)
Specifically:
Type mismatch between
m
and
len
Just prf => ?hole -- Just input
Using rewrite syntax from section 8.2 fixes the problem.
But order of len and m is important
`checkEqNat m len` would not work! (equational profs are not automatically symmetric -
sym function in 8.2)
TODO, also using Dec (section 8.3) fixes the problem, why?
This code compiles fine:
exactLength {m} len input = case decEq m len of
Yes Refl => Just input
No contra => Nothing
-}
exactLength : (len : Nat) -> (input : Vect m a) -> Maybe (Vect len a)
exactLength {m} len input
= case checkEqNat len m of
Nothing => Nothing
Just prf => rewrite prf in Just input -- syntax from 8.2
{-
`exactLength` implementation in the book (repeated below) does not need `rewrite` syntax.
Maybe because it keeps nat value in scope (look at SameNat constructor) and is Nat sepecific.
The need to have evidence of type/value being checked in scope seems to be important.
This relates to some of my Haskell experience (see F2 type family and solutions to example 1 and 2).
-}
data EqNat : (num1 : Nat) -> (num2 : Nat) -> Type where
SameNat : (num : Nat) -> EqNat num num
{- nicely generated by Idris by case splitting on third variable (eq) -}
sameS : (k : Nat) -> (j : Nat) -> (eq : EqNat k j) -> EqNat (S k) (S j)
sameS j j (SameNat j) = SameNat (S j)
checkEqNat1 : (num1 : Nat) -> (num2 : Nat) -> Maybe (EqNat num1 num2)
checkEqNat1 Z Z = Just (SameNat Z)
checkEqNat1 Z (S k) = Nothing
checkEqNat1 (S k) Z = Nothing
checkEqNat1 (S k) (S j) = case checkEqNat1 k j of
Nothing => Nothing
Just eq => Just (sameS _ _ eq)
{- The proof of equality allows this type of method to typecheck and
rewrite statement is not used. -}
exactLength1 : (len : Nat) -> (input : Vect m a) -> Maybe (Vect len a)
exactLength1 {m} len input
= case checkEqNat1 m len of
Nothing => Nothing
Just (SameNat len) => Just input
{- exercise 1, (x :) is just a function -}
same_cons : {xs : List a} -> {ys : List a} ->
xs = ys -> x :: xs = x :: ys
same_cons prf = cong prf
{- exercise 2, knowing that x's are indentical, this theorem reduces to same_cons -}
same_lists : {xs : List a} -> {ys : List a} ->
x = y -> xs = ys -> x :: xs = y :: ys
same_lists Refl = same_cons
{- exercise 3, 4 -}
data ThreeEqual : a -> b -> c -> Type where
Refl3 : ThreeEqual a a a
{- Idris knows that all 3 a's are the same, interstingly no need for cong -}
allSameS : (x, y, z : Nat) -> ThreeEqual x y z -> ThreeEqual (S x) (S y) (S z)
allSameS a a a Refl3 = Refl3As before, I try to keep Haskell code very close to Idris.
This code uses the programmable :~: type equality defined in Data.Type.Equality that is a close
equivalent of Idris' =
{-# LANGUAGE
GADTs
, DataKinds
, TypeOperators
, TypeFamilies
, PolyKinds
#-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
{-# OPTIONS_GHC -fwarn-unused-imports #-}
module Part2.Sec8_1_eqproof where
import Data.CodedByHand (Vect(..), Nat(..), SNat(..), vlength)
import Data.Type.Equality ((:~:)(Refl))
{- mimics concept of type level function in Idris-}
type family F (a :: k1) :: k2
-- | type family is a type level partial function so if x = y => f x = f y
-- not really needed (mimics Idris)
cong :: (x :~: y) -> F x :~: F y
cong Refl = Refl
checkEqNat :: SNat num1 -> SNat num2 -> Maybe (num1 :~: num2)
checkEqNat SZ SZ = Just Refl
checkEqNat SZ (SS k) = Nothing
checkEqNat (SS k) (SZ) = Nothing
checkEqNat (SS k) (SS j) = case checkEqNat k j of
Nothing -> Nothing
Just prf -> Just $ cong prf
-- Note: SS :: SNat n -> SNat ('S n) which explains the use of cong
type instance F n = 'S n
{-| Note, GHC can figure out cong on its own -}
checkEqNat' :: SNat num1 -> SNat num2 -> Maybe (num1 :~: num2)
checkEqNat' SZ SZ = Just Refl
checkEqNat' SZ (SS k) = Nothing
checkEqNat' (SS k) (SZ) = Nothing
checkEqNat' (SS k) (SS j) = case checkEqNat' k j of
Nothing -> Nothing
Just prf -> case prf of Refl -> Just Refl
exactLength :: SNat len -> Vect m a -> Maybe (Vect len a)
exactLength len vect = case checkEqNat (vlength vect) len of
Nothing -> Nothing
Just (Refl) -> Just vect
{- exercise examples -}
{-
type level partial application would be nice!
would make F2 redundant, this mimics Idris but is not really needed
-}
type family F2 (a :: k1) (b:: k2 ):: k3
{- I need z in scope for this to work -}
cong2 :: z -> (x :~: y) -> F2 z x :~: F2 z y
cong2 _ Refl = Refl
same_cons :: x -> xs :~: ys -> x ': xs :~: x ': ys
same_cons x prf = cong2 x prf
-- ^ cong2 is not needed as this works as well:
-- same_cons x Refl = Refl
type instance F2 x xs = x ': xs
{-| cong-less version -}
same_cons' :: x -> xs :~: ys -> x ': xs :~: x ': ys
same_cons' x prf = case prf of Refl -> Refl
{- again need value of at least one type in scope -}
same_lists :: x -> x :~: y -> xs :~: ys -> (x ': xs) :~: (y ': ys)
same_lists x Refl = same_cons x
data ThreeEqual a b c where
Refl3 :: ThreeEqual a a a
allSameS :: SNat x -> SNat y -> SNat z -> ThreeEqual x y z -> ThreeEqual ('S x) ('S y) ('S z)
allSameS _ _ _ Refl3 = Refl3
{- Good enough to have evidence of just one -}
allSameS2 :: SNat x -> ThreeEqual x y z -> ThreeEqual ('S x) ('S y) ('S z)
allSameS2 _ Refl3 = Refl3Maybe this are just basics but Haskell typechecker is great.
Why Proofs?
The book presents the need for proofs as a natural consequence of using dependent types.
This makes a lot of sense to me. If a type parameter has some underlying properties
(e.g. Vect is parametrized by n : Nat which comes with an algebra),
then it is only natural that the program will need to provide typechecker with some help
(like n + m = m + n).