342 views

Skip to first unread message

Feb 13, 2016, 12:21:00 PM2/13/16

to Idris Programming Language

Hi,

I'm writing a small article that touches on what dependent types are capable of. The problem is that although I have some background in Haskell, I'm quite new at this. I'm slowly making my way through some books on Coq and Agda, but right now I'm in over my head. :)

Here's what I'm working with: https://gist.github.com/KMahoney/b2a7856d179999daa2de

Now, in order to publish my article I don't actually need to provide the proofs (although that would be nice for me to understand), but I would like to fact check that

1) My types look plausible for what I'm trying to prove and

2) It is in fact possible to prove these properties.

Any advice or recommendations on reading material would be appreciated. I think I at least need a sigma in my 'justProof', because the 'r' has to come from somewhere, right?

Feb 13, 2016, 2:50:18 PM2/13/16

to idris...@googlegroups.com

Hi Kevin

> I'm writing a small article that touches on what dependent types are

> capable of. The problem is that although I have some background in Haskell,

> I'm quite new at this. I'm slowly making my way through some books on Coq

> and Agda, but right now I'm in over my head. :)

It's still a bit rough to get going with these things, unfortunately.

> Here's what I'm working

> with: https://gist.github.com/KMahoney/b2a7856d179999daa2de

>

> Now, in order to publish my article I don't actually need to provide the

> proofs (although that would be nice for me to understand), but I would like

> to fact check that

>

> 1) My types look plausible for what I'm trying to prove and

> 2) It is in fact possible to prove these properties.

I think that your types are close, but not correct for what you want.

This is because they are mixing two different notions of equality: the

built-in notion of equality in the type system, and the Boolean check

that a user implements as part of implementing Eq. Elem uses the

built-in notion of equality, while Eq can do basically anything.

Here's a counterexample for your nothingProof - a similar one could be

built for the other proof:

module Main

import Data.Vect

import Data.Fin

%default total

find : Eq x => List x -> x -> Maybe Int

find [] elem = Nothing

find (y :: xs) elem = if y == elem then (Just 0) else (map (\ n => n +

1) (find xs elem))

find2 : Eq x => {n : Nat} -> Vect n x -> x -> Maybe (Fin n)

find2 [] elem = Nothing

find2 (y :: xs) elem = if y == elem then (Just FZ) else (map FS (find2

xs elem))

ex : find2 [1, 2, 3] 2 = Just 1

ex = Refl

nothingProof : Eq x => (n : Nat) -> (v : Vect n x) -> (e : x) -> Not

(Elem e v) -> (find2 v e) = Nothing

nothingProof n v elem notIn = ?noIdea1

justProof : Eq x => (n : Nat) -> (v : Vect n x) -> (e : x) -> (find2 v e

= Just r) -> (index r v == e) = True

justProof n v elem findProof = ?noIdea2

data Counterexample : Type where

One : Counterexample

Two : Counterexample

implementation Eq Counterexample where

_ == _ = True

implementation Uninhabited (Just x = Nothing) where

uninhabited Refl impossible

nothingCounterexample : Void

nothingCounterexample =

absurd $ nothingProof _ [One] Two notIn

where notIn : Elem Two [One] -> Void

notIn Here impossible

notIn (There Here) impossible

What you probably should do, based on your stated goal, is to use the

DecEq interface instead of the Eq interface. This one is set up such

that its notion of equality _must_ correspond with the type theory's

notion of equality. Additionally, instead of returning Fin elements, try

returning an Elem proof directly - that has just as much information

about the position of the element in the Vect, because each Here or

There constructor corresponds to either an FS or an FZ constructor, but

it also guarantees the placement.

Here's an example of how it could work to find the Elem directly. I also

wrote a Maybe (Fin n) version that uses DecEq, and then proved the

lemmas that you wanted for your version. I put them in one proof instead

of two to save time and space - the type does a case analysis to figure

out which version it's working on.

I didn't use anything not in the Idris tutorial as far as I can see,

with the possible exception of the Uninhabited interface. The way that

works is this: a proof that something is impossible can go in an

Uninhabited implementation, and then "absurd" resolves that

implementation at a use site so we don't have to remember custom names

for all those lemmas.

Here's how I might do what you're going for, with a few explanatory

comments:

module Main

import Data.Vect

import Data.Fin

%default total

||| If a value is neither at the head of a Vect nor in the tail of

||| that Vect, then it is not in the Vect.

notHeadNotTail : Not (x = y) -> Not (Elem x xs) -> Not (Elem x (y :: xs))

notHeadNotTail notHead notTail Here = notHead Refl

notHeadNotTail notHead notTail (There tl) = notTail tl

||| Determine the first location of an element in a Vect. The types

||| guarantee that we find a valid index, but not that it's the first

||| occurrence.

find : DecEq a => (x : a) -> (xs : Vect n a) -> Dec (Elem x xs)

find x [] = No absurd

find x (y :: xs) with (decEq x y)

find x (x :: xs) | Yes Refl = Yes Here

find x (y :: xs) | No notHead with (find x xs)

find x (y :: xs) | No notHead | Yes prf = Yes (There prf)

find x (y :: xs) | No notHead | No notTail =

No $ notHeadNotTail notHead notTail

||| Find a Fin giving a position in a Vect, instead of an Elem

findIndex : DecEq a => (x : a) -> (xs : Vect n a) -> Maybe (Fin n)

findIndex x [] = Nothing

findIndex x (y :: xs) =

case decEq x y of

Yes _ => pure FZ

-- the following could be written as:

-- No _ => do tailIdx <- findIndex x xs

-- pure (FS tailIdx)

-- but idiom brackets are a bit cleaner:

No _ => [| FS (findIndex x xs) |]

-- (that was like the Haskell FS <$> findIndex x xs)

-- Prove that the Fin version corresponds to the Elem

-- version. Correspondence here means that if a Fin is found, we can

-- construct an Elem proof, and if a Fin is not found, then it is

-- provably impossible to construct an Elem proof.

findIndexOk : DecEq a => (x : a) -> (xs : Vect n a) ->

case findIndex x xs of

Just i => Elem x xs

Nothing => Not (Elem x xs)

findIndexOk x [] = absurd -- this is proved in the library already! :-)

findIndexOk x (y :: xs) with (decEq x y)

findIndexOk x (x :: xs) | Yes Refl = Here

findIndexOk x (y :: xs) | No notHead with (findIndexOk x xs) -- get an

induction hypothesis

findIndexOk x (y :: xs) | No notHead | ih with (findIndex x xs) --

split on the result of

--

the recursive call, to

--

reduce case expression

--

in the IH type

-- in this case, the induction hypothesis takes the second

-- branch in the case expression in the type, which tells us

-- that Not (Elem x xs)

findIndexOk x (y :: xs) | No notHead | ih | Nothing =

notHeadNotTail notHead ih

-- in this case, the IH tells us that it was indeed in the tail,

-- so we wrap in There to make it valid for y :: xs instead of

-- just xs

findIndexOk x (y :: xs) | No notHead | ih | Just z = There ih

(in case my mail client is being silly with line wraps, here's a gist

link: https://gist.github.com/david-christiansen/3b02d054b52405fecc70)

If that code doesn't make sense, I'd recommend working through the Idris

tutorial. If that doesn't clear things up, please ask further questions!

/David

> I'm writing a small article that touches on what dependent types are

> capable of. The problem is that although I have some background in Haskell,

> I'm quite new at this. I'm slowly making my way through some books on Coq

> and Agda, but right now I'm in over my head. :)

> Here's what I'm working

> with: https://gist.github.com/KMahoney/b2a7856d179999daa2de

>

> Now, in order to publish my article I don't actually need to provide the

> proofs (although that would be nice for me to understand), but I would like

> to fact check that

>

> 1) My types look plausible for what I'm trying to prove and

> 2) It is in fact possible to prove these properties.

This is because they are mixing two different notions of equality: the

built-in notion of equality in the type system, and the Boolean check

that a user implements as part of implementing Eq. Elem uses the

built-in notion of equality, while Eq can do basically anything.

Here's a counterexample for your nothingProof - a similar one could be

built for the other proof:

module Main

import Data.Vect

import Data.Fin

%default total

find : Eq x => List x -> x -> Maybe Int

find [] elem = Nothing

find (y :: xs) elem = if y == elem then (Just 0) else (map (\ n => n +

1) (find xs elem))

find2 : Eq x => {n : Nat} -> Vect n x -> x -> Maybe (Fin n)

find2 [] elem = Nothing

find2 (y :: xs) elem = if y == elem then (Just FZ) else (map FS (find2

xs elem))

ex : find2 [1, 2, 3] 2 = Just 1

ex = Refl

nothingProof : Eq x => (n : Nat) -> (v : Vect n x) -> (e : x) -> Not

(Elem e v) -> (find2 v e) = Nothing

nothingProof n v elem notIn = ?noIdea1

justProof : Eq x => (n : Nat) -> (v : Vect n x) -> (e : x) -> (find2 v e

= Just r) -> (index r v == e) = True

justProof n v elem findProof = ?noIdea2

data Counterexample : Type where

One : Counterexample

Two : Counterexample

implementation Eq Counterexample where

_ == _ = True

implementation Uninhabited (Just x = Nothing) where

uninhabited Refl impossible

nothingCounterexample : Void

nothingCounterexample =

absurd $ nothingProof _ [One] Two notIn

where notIn : Elem Two [One] -> Void

notIn Here impossible

notIn (There Here) impossible

What you probably should do, based on your stated goal, is to use the

DecEq interface instead of the Eq interface. This one is set up such

that its notion of equality _must_ correspond with the type theory's

notion of equality. Additionally, instead of returning Fin elements, try

returning an Elem proof directly - that has just as much information

about the position of the element in the Vect, because each Here or

There constructor corresponds to either an FS or an FZ constructor, but

it also guarantees the placement.

Here's an example of how it could work to find the Elem directly. I also

wrote a Maybe (Fin n) version that uses DecEq, and then proved the

lemmas that you wanted for your version. I put them in one proof instead

of two to save time and space - the type does a case analysis to figure

out which version it's working on.

I didn't use anything not in the Idris tutorial as far as I can see,

with the possible exception of the Uninhabited interface. The way that

works is this: a proof that something is impossible can go in an

Uninhabited implementation, and then "absurd" resolves that

implementation at a use site so we don't have to remember custom names

for all those lemmas.

Here's how I might do what you're going for, with a few explanatory

comments:

module Main

import Data.Vect

import Data.Fin

%default total

||| If a value is neither at the head of a Vect nor in the tail of

||| that Vect, then it is not in the Vect.

notHeadNotTail : Not (x = y) -> Not (Elem x xs) -> Not (Elem x (y :: xs))

notHeadNotTail notHead notTail Here = notHead Refl

notHeadNotTail notHead notTail (There tl) = notTail tl

||| Determine the first location of an element in a Vect. The types

||| guarantee that we find a valid index, but not that it's the first

||| occurrence.

find : DecEq a => (x : a) -> (xs : Vect n a) -> Dec (Elem x xs)

find x [] = No absurd

find x (y :: xs) with (decEq x y)

find x (x :: xs) | Yes Refl = Yes Here

find x (y :: xs) | No notHead with (find x xs)

find x (y :: xs) | No notHead | Yes prf = Yes (There prf)

find x (y :: xs) | No notHead | No notTail =

No $ notHeadNotTail notHead notTail

||| Find a Fin giving a position in a Vect, instead of an Elem

findIndex : DecEq a => (x : a) -> (xs : Vect n a) -> Maybe (Fin n)

findIndex x [] = Nothing

findIndex x (y :: xs) =

case decEq x y of

Yes _ => pure FZ

-- the following could be written as:

-- No _ => do tailIdx <- findIndex x xs

-- pure (FS tailIdx)

-- but idiom brackets are a bit cleaner:

No _ => [| FS (findIndex x xs) |]

-- (that was like the Haskell FS <$> findIndex x xs)

-- Prove that the Fin version corresponds to the Elem

-- version. Correspondence here means that if a Fin is found, we can

-- construct an Elem proof, and if a Fin is not found, then it is

-- provably impossible to construct an Elem proof.

findIndexOk : DecEq a => (x : a) -> (xs : Vect n a) ->

case findIndex x xs of

Just i => Elem x xs

Nothing => Not (Elem x xs)

findIndexOk x [] = absurd -- this is proved in the library already! :-)

findIndexOk x (y :: xs) with (decEq x y)

findIndexOk x (x :: xs) | Yes Refl = Here

findIndexOk x (y :: xs) | No notHead with (findIndexOk x xs) -- get an

induction hypothesis

findIndexOk x (y :: xs) | No notHead | ih with (findIndex x xs) --

split on the result of

--

the recursive call, to

--

reduce case expression

--

in the IH type

-- in this case, the induction hypothesis takes the second

-- branch in the case expression in the type, which tells us

-- that Not (Elem x xs)

findIndexOk x (y :: xs) | No notHead | ih | Nothing =

notHeadNotTail notHead ih

-- in this case, the IH tells us that it was indeed in the tail,

-- so we wrap in There to make it valid for y :: xs instead of

-- just xs

findIndexOk x (y :: xs) | No notHead | ih | Just z = There ih

(in case my mail client is being silly with line wraps, here's a gist

link: https://gist.github.com/david-christiansen/3b02d054b52405fecc70)

If that code doesn't make sense, I'd recommend working through the Idris

tutorial. If that doesn't clear things up, please ask further questions!

/David

Feb 13, 2016, 3:36:08 PM2/13/16

to Idris Programming Language

Thank you David, that's really helpful!

In any case, your type signature for findIndexOk is enough for me to complete my article. I will link to your post for readers curious enough for a full explanation.

At first I was confused why 'Eq' is not good enough, but I think I have it. Am I right in thinking that another way around that would be to keep the 'Eq' typeclass, but instead of 'Elem' for the proof, using something like 'Any (/x => x == elem)' ?

I think I understand the approach to the proof, if not the details, and in fact I'd noticed the relationship between Fin and the Elem constructors myself. I just didn't know how to use it!

In any case, your type signature for findIndexOk is enough for me to complete my article. I will link to your post for readers curious enough for a full explanation.

Feb 13, 2016, 3:46:44 PM2/13/16

to idris...@googlegroups.com

On Sat, Feb 13, 2016 at 12:36 PM, Kevin Mahoney <ke...@kevinmahoney.co.uk> wrote:

At first I was confused why 'Eq' is not good enough, but I think I have it.

In short: 'Eq' is not specific enough. You can implement 'Eq' to do anything at all, including returning true for any combination of inputs. That means it (1) isn't guaranteed to match the type system's notion of equality as used by Elem, and (2) is often less useful for proofs in general, because it's less strict.

As David said, DecEq is designed in a way where you *can't *implement it in a ridiculous way. (Well, without some serious gymnastics.) In addition to the "equality" result, an implementation of 'decEq' hands back a proof of type system equality that the type checker (and thus proofs) will accept.

Having both concepts in the language tends to confuse noobs, and can lead to impedance mismatches in real programs (where one module is using Eq and the other needs DecEq). But it's not clear that we could, say, discard Eq, in part because implementations may be more efficient than DecEq, and in part because you can't currently use a decEq result in an if statement. :-)

-Cliff

Feb 13, 2016, 4:11:49 PM2/13/16

to idris...@googlegroups.com

On 13/02/16 15:36, Kevin Mahoney wrote:

> Thank you David, that's really helpful!

Glad to hear it!
> Thank you David, that's really helpful!

> At first I was confused why 'Eq' is not good enough, but I think I have it.

> Am I right in thinking that another way around that would be to keep the

> 'Eq' typeclass, but instead of 'Elem' for the proof, using something like

> 'Any (/x => x == elem)' ?

> I think I understand the approach to the proof, if not the details, and in

> fact I'd noticed the relationship between Fin and the Elem constructors

> myself. I just didn't know how to use it!

mathematical proofs unless you really squint. Hopefully the comments

bridged the gap a bit.

> In any case, your type signature for findIndexOk is enough for me to

> complete my article. I will link to your post for readers curious enough

> for a full explanation.

few times, so hopefully it's not just nonsense in their ears.

/David

Feb 13, 2016, 4:17:28 PM2/13/16

to idris...@googlegroups.com

On 13/02/16 15:46, Cliff L. Biffle wrote:

> Having both concepts in the language tends to confuse noobs, and can lead

> to impedance mismatches in real programs (where one module is using Eq and

> the other needs DecEq). But it's not clear that we could, say, discard Eq,

> in part because implementations may be more efficient than DecEq, and in

> part because you can't currently use a decEq result in an if statement. :-)

Even worse: DecEq may be too specific for some uses, and ensuring
> Having both concepts in the language tends to confuse noobs, and can lead

> to impedance mismatches in real programs (where one module is using Eq and

> the other needs DecEq). But it's not clear that we could, say, discard Eq,

> in part because implementations may be more efficient than DecEq, and in

> part because you can't currently use a decEq result in an if statement. :-)

consistency between Eq and DecEq may make programs slower.

For many types, we want an equality that is coarser than the built-in

one. For instance, we might want it to be alpha-equivalence for lambda

terms, or set equality for a tree type. DecEq forces us to keep these

separate, or even worse, to make our data representation be dictated by

the needs of type checking, which might come in conflict with other

considerations, such as performance or ease of error reporting. Quotient

types or setoids would fix this, at the cost of massive tedium.

Also, in Idris, constructor fields not used at runtime are erased.

However, the type system doesn't really know about this. If we use

DecEq, then it may have to inspect all the fields of the constructor.

This means that they are suddenly _all_ runtime-relevant, which can

potentially make them much slower.

/David

Feb 15, 2016, 5:35:20 PM2/15/16

to Idris Programming Language

David,

does your gist compile for you?

For (reduced by me)

find : DecEq a => (x : a) -> (xs : Vect n a) -> Dec (Elem x xs)

find x [] = No absurd

find x (y :: xs) = ?hole

I get the compiler error

When checking argument contra to constructor Prelude.Basics.No:

Can't find implementation for Uninhabited (Elem x [])

Regards

Markus

Mar 4, 2016, 9:20:53 AM3/4/16

to idris...@googlegroups.com, Kevin Mahoney

Kevin,

your |justProof| looks quite similar to our

> lookupIndexLemma : (k : Fin n) ->

> (xs : Vect n t) ->

> (p : Injective2 xs) ->

> (q : Elem (index k xs) xs) ->

> lookup (index k xs) xs q = k

If you take a look at

https://github.com/nicolabotta/SeqDecProbs/blob/master/frameworks/14-/VectOperations.lidr

https://github.com/nicolabotta/SeqDecProbs/blob/master/frameworks/14-/VectProperties.lidr

you will find an implementation of |lookupIndexLemma| and some more

properties of vectors.

Best,

Nicola

> --

> You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.

> To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com.

> For more options, visit https://groups.google.com/d/optout.

>

your |justProof| looks quite similar to our

> lookupIndexLemma : (k : Fin n) ->

> (xs : Vect n t) ->

> (p : Injective2 xs) ->

> (q : Elem (index k xs) xs) ->

> lookup (index k xs) xs q = k

If you take a look at

https://github.com/nicolabotta/SeqDecProbs/blob/master/frameworks/14-/VectOperations.lidr

https://github.com/nicolabotta/SeqDecProbs/blob/master/frameworks/14-/VectProperties.lidr

you will find an implementation of |lookupIndexLemma| and some more

properties of vectors.

Best,

Nicola

> You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.

> To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com.

> For more options, visit https://groups.google.com/d/optout.

>

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu