I don't know the formal definition, but dependent types seem analogous to checking an invariant at runtime. -deech On Tue, Dec 21, 2010 at 5:53 AM, Patrick Browne wrote:

Hi, In a previous posting[1] I asked was there a way to achieve a proof of mirror (mirror x) = x

in Haskell itself. The code for the tree/mirror is below:

 module BTree where  data Tree a = Tip | Node (Tree a) a (Tree a)

 mirror ::  Tree a -> Tree a  mirror (Node x y z) = Node (mirror z) y (mirror x)  mirror Tip = Tip

The reply from Eugene Kirpichov was:

...

...

It is not possible at the value level, because Haskell does not support dependent types and thus cannot express the type of the proposition "forall a . forall x:Tree a, mirror (mirror x) = x", and therefore a proof term also cannot be constructed.

Could anyone explain what *dependent types* mean in this context? What is the exact meaning of forall a and forall x?

Thanks, Pat [1] http://www.mail-archive.com/haskell-cafe@haskell.org/msg64842.html

This message has been scanned for content and viruses by the DIT Information Services E-Mail Scanning Service, and is believed to be clean. http://www.dit.ie

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Patrick, Dependent types are program types that depend on runtime values. That is, they are essentially a type of the form: f :: (a :: X) -> T where 'a' is a *value* of type 'X', which is mentioned in the *type* 'T'. You do not see such things in Haskell, because Haskell separates values from types - the language of runtime values, and the language of compile-time values are separate by design. In dependently typed languages, values and types are in fact, the same terms and part of the same language, not separated by compiler phases. The distinction between runtime and compile time becomes blurry at this stage. By the Curry-Howard isomorphism, we would like to make a proof of some property, particularly that "mirror (mirror x) = x" - but by CH, types are the propositions we must prove, and values are the terms we must prove them with (such as in first-order or propositional logics.) This is what Eugene means when he says it is not possible to prove this at the value level. Haskell cannot directly express the following type: forall a. forall x:Tree a, mirror (mirror x) = x We can think of the 'forall' parts of the type as bringing the variables 'a' and 'x' into scope with fresh names, and they are universally quantified so that this property is established for any given value of type 'a'. As you can see, this is a dependent type - we establish we will be using something of type a, and then we establish that we also have a *value* x of type 'Tree a', which is mentioned finally by saying that 'mirror (mirror x) = x'. Because we cannot directly express the above type (as we cannot mix runtime values and type level values) we cannot also directly express a proof of such a proposition directly in Haskell. However, if we can express such a type - that is, a type which can encode the 'Mirror' function - it is possible to construct a value-level term which is a proof of such a proposition. By CH, this is also possible, only not nearly as palatable because we encode the definition of 'mirror' at the value level as well as the type level - again, types and values in haskell exist in different realms. With dependent types we only need to write 'mirror' *once* because we can use it at both the type and value level. Also, because dependently typed languages have more expressive type systems in general, it quickly becomes a burden to do dependent-type 'tricks' in Haskell, although some are manageable. For amusement, I went ahead and actually implemented 'Mirror' as a type family, and used a little bit of hackery thanks to GHC to prove that indeed, 'mirror x (mirror x) = x' since with a type family we can express 'mirror' as a type level function via type families. It uses Ryan Ingram's approach to lightweight dependent type programming in Haskell. https://gist.github.com/750279 As you can see, it is quite unsatisfactory since we must encode Mirror at the type level, as well as 'close off' a typeclass to constrain the values over which we can make our proof (in GHC, typeclasses are completely open and can have many nonsensical instances. We could make an instance for, say 'Mirror Int = Tip', for example, which breaks our proof. Ryan's trick is to encode 'closed' type classes by using a type class that implements a form of 'type case', and any instances must prove that the type being instantiated is either of type 'Tip' or type 'Node' by parametricity.) And well, the tree induction step is just a little bit painful, isn't it? So that's an answer, it's just probably not what you wanted. However, at one point I wrote about proving exactly such a thing (your exact code, coincidentally) in Haskell, only using an 'extraction tool' that extracts Isabelle theories from Haskell source code, allowing you to prove such properties with an automated theorem prover. http://hacks.yi.org/~as/posts/2009-04-20-A-little-fun.html Of course, this depends on the extractor tool itself being correct - if it is not, it could incorrectly translate your Haskell to similar but perhaps subtly wrong Isabelle code, and then you'll be proving the wrong thing! Haskabelle also does support much more than Haskell98 if I remember correctly, although that may have changed. I also remember reading that Galois has a project of having 'provable haskell' using Isabelle, but I can't verify that I suppose. On Tue, Dec 21, 2010 at 5:53 AM, Patrick Browne wrote:

Hi, In a previous posting[1] I asked was there a way to achieve a proof of mirror (mirror x) = x

in Haskell itself. The code for the tree/mirror is below:

 module BTree where  data Tree a = Tip | Node (Tree a) a (Tree a)

 mirror ::  Tree a -> Tree a  mirror (Node x y z) = Node (mirror z) y (mirror x)  mirror Tip = Tip

The reply from Eugene Kirpichov was:

...

...

It is not possible at the value level, because Haskell does not support dependent types and thus cannot express the type of the proposition "forall a . forall x:Tree a, mirror (mirror x) = x", and therefore a proof term also cannot be constructed.

Could anyone explain what *dependent types* mean in this context? What is the exact meaning of forall a and forall x?

Thanks, Pat [1] http://www.mail-archive.com/haskell-cafe@haskell.org/msg64842.html

This message has been scanned for content and viruses by the DIT Information Services E-Mail Scanning Service, and is believed to be clean. http://www.dit.ie

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

-- Regards, Austin

On Tuesday 21 December 2010 19:34:11, Felipe Almeida Lessa wrote:

Theorem mirror_mirror : forall A (x : Tree A), mirror (mirror x) = x. induction x; simpl; auto. rewrite IHx1; rewrite IHx2; trivial. Qed.

Since mirror (mirror x) = x doesn't hold in Haskell, I take it that Coq doesn't allow infinite structures?

On Tuesday 21 December 2010 20:11:37, Colin Paul Adams wrote:

...

...

...

...

...

"Daniel" == Daniel Fischer writes:

Daniel> On Tuesday 21 December 2010 19:34:11, Felipe Almeida Lessa wrote:

...

Theorem mirror_mirror : forall A (x : Tree A), mirror (mirror x) = x.

>> induction x; simpl; auto. rewrite IHx1; rewrite IHx2; trivial. >> Qed.

Daniel> Since mirror (mirror x) = x doesn't hold in Haskell, I take Daniel> it that Coq doesn't allow infinite structures?

Why doesn't it hold?

Hit send before I finished thinking, it should hold.

On Tue, Dec 21, 2010 at 5:02 PM, Daniel Fischer wrote:

On Tuesday 21 December 2010 19:34:11, Felipe Almeida Lessa wrote:

...

Theorem mirror_mirror : forall A (x : Tree A), mirror (mirror x) = x.   induction x; simpl; auto.   rewrite IHx1; rewrite IHx2; trivial. Qed.

Since mirror (mirror x) = x doesn't hold in Haskell, I take it that Coq doesn't allow infinite structures?

Even if the theorem does hold with infinite structures, I don't really know the answer to your question. I'm just starting to study Coq in my free time =). My guess would be "no", because functions need to be total. But that's just a wild guess, and you shouldn't take my word for it =). Cheers! -- Felipe.

I think it's pretty legit. You aren't actually making a claim about the values in the tree but I think parametricity handles that for you, especially since you have existential types for the payload at every tree level (so you can't go shuffling those around). The only thing missing (and that you can't change in Haskell) is that your statement is about Mirror (Mirror x) == x, rather than mirror (mirror x) == x. mirror gives you Mirror but there's currently no proof to show that it's the only way to do it, so there's a missing step there, I think. Anyway, for those talking about the coinductive proof, I made one in Agda: http://hpaste.org/42516/mirrormirror Simulating bottoms wouldn't be too hard, but I don't think the statement is even true in the presence of bottoms, is it? Dan On Thu, Dec 23, 2010 at 9:27 AM, Sjoerd Visscher wrote:

On Dec 21, 2010, at 6:57 PM, austin seipp wrote:

...

https://gist.github.com/750279

I took Austins code and modified it to run on a Tree GADT which is parameterized by its shape:

https://gist.github.com/752982

Would this count as a function mirror with proof that mirror (mirror x) == x?

-- Sjoerd Visscher

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Fair enough :) that'll teach me to hypothesize something without thinking about it! I guess I could amend my coinductive proof: http://hpaste.org/paste/42516/mirrormirror_with_bottom#p42517 does that cover bottom-ness adequately? I can't say I've thought through it terribly carefully. On Thu, Dec 23, 2010 at 12:30 PM, Ryan Ingram wrote:

On Thu, Dec 23, 2010 at 8:19 AM, Daniel Peebles wrote:

...

Simulating bottoms wouldn't be too hard, but I don't think the statement is even true in the presence of bottoms, is it?

Isn't it?

data Tree a = Tip | Node (Tree a) a (Tree a)

mirror :: Tree a -> Tree a mirror Tip = Tip mirror (Node x y z) = Node (mirror z) y (mirror x)

--

-- base cases mirror (mirror _|_) = mirror _|_ = _|_

mirror (mirror Tip) = mirror Tip = Tip

-- inductive case mirror (mirror (Node x y z)) = mirror (Node (mirror z) y (mirror x)) = Node (mirror (mirror x)) y (mirror (mirror z)) -- induction = Node x y z

-- ryan

On Tue, Dec 21, 2010 at 9:57 AM, austin seipp wrote:

For amusement, I went ahead and actually implemented 'Mirror' as a type family, and used a little bit of hackery thanks to GHC to prove that indeed, 'mirror x (mirror x) = x' since with a type family we can express 'mirror' as a type level function via type families. It uses Ryan Ingram's approach to lightweight dependent type programming in Haskell.

https://gist.github.com/750279

Thanks for the shout out :) I think the type of your proof term is incorrect, though; it requires the proof to be passed in, which is sort of a circular logic. The type you want is proof1 :: forall r x. BinTree x => ((x ~ Mirror (Mirror x)) => x -> r) -> r proof1 t k = ... Alternatively, data TypeEq a b where Refl :: TypeEq a a proof1 :: forall x. BinTree x => x -> TypeEq (Mirror (Mirror x)) x proof1 t = ... Here's an implementation for the latter newtype P x = P { unP :: TypeEq (Mirror (Mirror x)) x } baseCase :: P Tip baseCase = P Refl inductiveStep :: forall a b c. P a -> P c -> P (Node a b c) inductiveStep (P Refl) (P Refl) = P Refl proof1 t = unP $ treeInduction t baseCase inductiveStep (I haven't tested this, but I believe it should work) -- ryan

On Tue, Dec 21, 2010 at 08:31:08AM -0700, Jonathan Geddes wrote:

I'd love for the compiler to give an error (or maybe just a warning) in the case that I have a pattern match in a monad that just blows up (throws an exception) on a pattern match failure.

You will be interested to know that everything you ask for already was in Haskell ages ago: http://www.cs.auckland.ac.nz/references/haskell/haskell-report-1.4-html/exps... They decided to get rid of it in Haskell 98, for reasons that someone else can probably explain. Lauri