oh : so True (a question)

[Falko]

Hello,

I want to play with the example from tutorial 3.8, but don't get it compiled. (I hope it's not just a stupid typo ..)

1. Substitute for unsafeDrawPoint

> udp : Int -> Int -> String
> udp a b = "Hello"

2. A check:

> checker : Int -> Int -> Bool
> checker a b = a >= 0 && a < 100 && b >= 0 && b < 100

3. And here, the implementation doesn't type check:

> dp : (x : Int) -> (y : Int) -> so (checker x y) -> String
> dp x y oh = udp x y

And the message is still completely greek to me:

Can't unify so True with so (Builtins.!>#@Builtins.Ord$[Int] x 0 (boolElim (intToBool (prim__eqInt x 0)) EQ (boolElim (intToBool (prim__ltInt x 0)) Builtins.LT Builtins.GT)) || (intToBool (prim__eqInt x 0)) && (Builtins.!<#@Builtins.Ord$[Int] x 100 (boolElim (intToBool (prim__eqInt x 100)) EQ (boolElim (intToBool (prim__ltInt x 100)) Builtins.LT Builtins.GT))) && (Builtins.!>#@Builtins.Ord$[Int] y 0 (boolElim (intToBool (prim__eqInt y 0)) EQ (boolElim (intToBool (prim__ltInt y 0)) Builtins.LT Builtins.GT)) || (intToBool (prim__eqInt y 0))) && (Builtins.!<#@Builtins.Ord$[Int] y 100 (boolElim (intToBool (prim__eqInt y 100)) EQ (boolElim (intToBool (prim__ltInt y 100)) Builtins.LT Builtins.GT))))

Specifically:
    Can't unify True with Builtins.!>#@Builtins.Ord$[Int] x 0 (boolElim (intToBool (prim__eqInt x 0)) EQ (boolElim (intToBool (prim__ltInt x 0)) Builtins.LT Builtins.GT)) || (intToBool (prim__eqInt x 0)) && (Builtins.!<#@Builtins.Ord$[Int] x 100 (boolElim (intToBool (prim__eqInt x 100)) EQ (boolElim (intToBool (prim__ltInt x 100)) Builtins.LT Builtins.GT))) && (Builtins.!>#@Builtins.Ord$[Int] y 0 (boolElim (intToBool (prim__eqInt y 0)) EQ (boolElim (intToBool (prim__ltInt y 0)) Builtins.LT Builtins.GT)) || (intToBool (prim__eqInt y 0))) && (Builtins.!<#@Builtins.Ord$[Int] y 100 (boolElim (intToBool (prim__eqInt y 100)) EQ (boolElim (intToBool (prim__ltInt y 100)) Builtins.LT Builtins.GT)))

Thank you, Falko

[Daniel Peebles]

I'm not an experienced idris-er, but in Agda at least you'd need to introduce `checker x y` into the pattern matching scope before you could match on `oh` (so that it could be refined to `True`). You'd do that using a `with` block. As it stands, matching on the `oh` constructor there is saying "some complex expression that isn't in scope is equal to `True`". I'm not sure if that is the actual reason for the error message in idris, as it might be more lax about those kinds of requirements, but it seems likely that it might be the cause.

In your particular case, what does pattern matching on `oh` get you? The main benefit is the knowledge that `checker x y` is `True`, but you don't use that knowledge in your function.

In general, even if you were to use that knowledge, it wouldn't be in the most easy-to-consume form. Booleans are remarkably uninformative in general, and even if you did know that your expression was true, you'd have to work backwards from that fact to do most useful things with it. In your example, what you'd really want for proofs is a 4-tuple with four proofs of boundedness in it, that you could use individually; the `Bool` gives you none of those, and would only allow you to separately obtain a 4-tuple by doing more work (work that you could have done in the first place when producing the `Bool`).

[Falko]

Hello Daniel,

I probably have to read more to completely understand your answer. My question was about page 14 of the tutorial - and that's all of my experience concerning dependently typed programming :-)

My interpretation of the example (and I mainly just copied it - lazily using shorter names) is, that the last method can only be called when the compiler is sure about a successful check.

But well, still learning.

Thank you for the response. (and I will read it again when "proof in idris" means something for me. Promised! :)

Regards, Falko

[Falko]

An example that works (from 6.1 of the tutorial):

> fact : Int -> Int
> fact 0 = 1
> fact 1 = 1
> fact n = n * (fact (n - 1))

> compileTimeTestFact : so (fact 4 == 24)
> compileTimeTestFact = oh

As intended: after changing 24 to 42 the code will not parse.

I still don't know how to generalise this to understand the start problem.

Regards, Falko

[Cezar Ionescu]

Falko <falko....@gmail.com> wrote:

> 3. And here, the implementation doesn't type check:
> > dp : (x : Int) -> (y : Int) -> so (checker x y) -> String
> > dp x y oh = udp x y
> And the message is still completely greek to me:

> [snip!]

I think you're right, it should work (after all, it's in the tutorial!),
so you've discovered another bug. Strangely enough, replacing the |oh|
with an underscore will make it type check...

Best,
Cezar.

[Edwin Brady]

Actually I think the bug here is in the tutorial… in general, the elaborator doesn't know that checker x y = True, so you can't have 'oh' there. You'll need an _ or some variable instead. Pretty much what Daniel said earlier.

Edwin.

[Cezar Ionescu]

> Actually I think the bug here is in the tutorial… in general, the
> elaborator doesn't know that checker x y = True, so you can't have
> 'oh' there. You'll need an _ or some variable instead. Pretty much
> what Daniel said earlier.

I'm ashamed to say Daniel's argument didn't get through to me either. I
stopped at "at least in Agda, you'd have to...". I actually tested the
example in Agda, and it worked with no changes. No |with| needed.

Best,
Cezar.

[Daniel Peebles]

The last method can only be called when you provide a proof that your parameters pass the requirements of checker, but that doesn't mean you need to actually match on the `oh` constructor. Pattern matching on constructors of inductive families (data types that refine parameters) introduces implicit knowledge about equalities into scope. For example, in Haskell with GADTs:

data Moo a where

  Baa :: Moo Int

foo :: Moo a -> a

foo _ = 5 -- this fails

bar :: Moo a -> a

bar Baa = 5 -- this passes

In your case, pattern matching on the `oh` constructor is telling idris that "checker x y` is `True`, but `checker x y` is a complex expression. This would cause Agda great distress, because it would say "you're telling me something is equal to True, but I can't represent that knowledge anywhere in my pattern!! what can I do??"

The Haskell example above would work in Agda too because that universally quantified `a` variable in the type acts like an implicit Set-valued variable, and can be implicitly refined. So if we expand implicits:

bar : {a : Set} -> Moo a -> a

bar {.Int} Baa = 5

where that period in front of `Int` is acknowledging that the value in that pattern is forced by another pattern (`Baa` right after it) to be `Int`.

So what we have is that `Baa` is a constructor that carries a magic equality proof with it, and if we want to pattern match on it, we need to be able to add a dotted pattern as we did above, somewhere in the patterns in scope. If pattern-matching on such a constructor would result in no dots being added anywhere (because the expression in question isn't in scope in the pattern) then Agda will not like it. So Agda would reject your example with `so (checker x y)` for that reason, because `oh` carries the proof that `checker x y = True`, and `checker x y` is not in scope. To bring it into scope, we'd do something like:

dp : (x : Int) -> (y : Int) -> so (checker x y) -> String

dp x y q with checker x y

dp x y oh | .True = udp x y

so the dottedness of the match on `oh` is respected. That is, you're acknowledging that you know that `checker x y` must be true when you pattern match on that `oh`.

Anyway, that's an explanation of the reasoning behind Agda. It's a bit of a design decision, but I imagine similar issues arise in Idris and even if dot patterns are not present (I'm not sure they are?), you're still introducing knowledge about something complex and that can cause trouble.

In your particular case, you can just completely ignore the value (with a wildcard pattern of some sort) of the `so (checker x y)`. You've required that your caller pass it to you, and as long as they do that, you don't really care what's in it because your function doesn't use the proof. 

[Daniel Peebles]

Can we see the relevant Agda code?

[Daniel Peebles]

For reference, this is how I would translate the relevant concept to Agda, and it behaves as I described earlier:

module SoTrue where

data Bool : Set where

  false true : Bool

data so : Bool → Set where

  oh : so true

data Nat : Set where

  zero : Nat

  suc  : Nat → Nat

_isZero : Nat → Bool

zero isZero = true

suc _ isZero = false

{-

foo : (x : Nat) → so (x isZero) → Nat

foo x oh = ?

-- true != x isZero of type Bool

-- when checking that the pattern oh has type so (x isZero)

-}

bar : (x : Nat) → so (x isZero) → Nat

bar x q with x isZero

bar x oh | .true = x

On Sun, Nov 25, 2012 at 4:34 PM, Cezar Ionescu <ion...@pik-potsdam.de> wrote:

[Cezar Ionescu]

Daniel Peebles <pumpk...@gmail.com> wrote:

> Can we see the relevant Agda code?

Well, I was just about to post that: it turns out I managed to misspell
oh when defining |so| (not in-built in Agda). I called it |o| instead.
So the |oh| from the cut-n-paste from Falko's code was just a variable
name. With the correction, you're right: Agda rejects it as well.
Sorry for the error!

Best,
Cezar.

[Edwin Brady]

Following this discussion, I've made a couple of small changes (in HEAD).

1. You should get a better error message now. The problem is that you're seeing terms in normal form, rather than what you actually wrote. Now you'll get a description of the top level unification failure (which will not normalise checker x y) and a more specific error, which says exactly what the problem was.

2. I've fixed the mistake in the tutorial!

Edwin.

[Adam Wall]

Hi Edwin, I just started playing with Idris (a long time Haskell user), and have some questions about the "so" type. I apologize if this is the wrong medium for this question, but there's not too much information about Idris on the web yet.

I wrote a silly program to test this out:

underTen : Int -> Bool

underTen x = x < 10

printOnlyIfUnderTen : (x : Int) -> so (underTen x) -> IO ()

printOnlyIfUnderTen x _ = print x

{- This works as I expect -}

test1 : IO ()

test1 = printOnlyIfUnderTen 8 oh

{- This fails to compile -}

test2 : IO ()

test2 = printOnlyIfUnderTen 11 oh

{- This fails to compile -}

test3 : IO ()

test3 = do x <- return 8

           printOnlyIfUnderTen x oh

{- This is what I WANT to write, not sure how to get there? -}

test4 : IO ()

test4 = do x <- return 8

           if (underTen x)

               then printOnlyIfUnderTen x oh

               else putStrLn "not under ten"

Basically, in test4... how do I supply the proof "underTen x", within the scope of my if statement?

[Edwin Brady]

Hi Adam,
This is a good medium to ask the question!

The problem is that a Bool doesn't tell you anything about where it came from - that is, why it's True or False. Not only that, the type of "if…then…else" is the same in each branch, and doesn't depend on the Bool it checks, so that information has gone.

One possibility is to use the following function:

> :t choose
Prelude.Either.choose : (b : Bool) -> Either (so b) (so (not b))

This generates either a proof that 'b' is true or not. I will leave some spoiler space so as not to give away the answer too easily - my definition of test4 is below the quoted text. Hope this helps!

Edwin.

> --
> 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/groups/opt_out.

My definition:

test4 : IO ()
test4 = do x <- return 8

case choose (underTen x) of
Left p => printOnlyIfUnderTen x p
Right p => putStrLn "not under ten"

[Adam Wall]

Thanks Edwin, 'choose' is exactly what I was looking for. This enables a very cool style of programming, where all pre-conditions to a function can be verified at compile-time; this eliminates the need for exceptions and the compiler can guarantee the non-existence of most runtime errors (I think running out of memory, and failing with calls to unsafe C code are the only exceptions). I'm looking forward to writing more Idris code and hopefully contributing to the project once I understand it a bit more; impressive work!

On Fri, Feb 7, 2014 at 4:28 PM, Edwin Brady <edwin...@gmail.com> wrote:

Hi Adam,
This is a good medium to ask the question!

The problem is that a Bool doesn't tell you anything about where it came from - that is, why it's True or False. Not only that, the type of "if...then...else" is the same in each branch, and doesn't depend on the Bool it checks, so that information has gone.

--
You received this message because you are subscribed to a topic in the Google Groups "Idris Programming Language" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/idris-lang/2xzKAtVoxQM/unsubscribe.
To unsubscribe from this group and all its topics, send an email to idris-lang+...@googlegroups.com.

[Chris Warburton]

Adam Wall <agc...@gmail.com> writes:

> Thanks Edwin, 'choose' is exactly what I was looking for. This enables a
> very cool style of programming, where all pre-conditions to a function can
> be verified at compile-time; this eliminates the need for exceptions and
> the compiler can guarantee the non-existence of most runtime errors (I
> think running out of memory, and failing with calls to unsafe C code are
> the only exceptions). I'm looking forward to writing more Idris code and
> hopefully contributing to the project once I understand it a bit more;
> impressive work!

Another good use of 'choice' and 'so' is in unit tests. In most
languages we can write a suite of unit tests which give back booleans:

double : Nat -> Nat
double x = x + x

doubleTwoTest : Bool
doubleTwoTest = double 2 == 4

In dependently typed languages like Idris we can go one step further and
enforce these tests at compile-time:

doubleTwoProof : so (double 2 == 4)
doubleTwoProof = oh

No more work is involved, since the only 'proof step' required is
computing the results of "double" and "==" then unifying it with True,
which the compiler will do automatically without asking.

Cheers,
Chris

[David Christiansen]

A downside of this approach in Idris is that it will only work for total functions. Non-total funs won't reduce, so they won't unify with True.

/David

[Matus Tejiscak]

Quoting Chris Warburton <chris...@googlemail.com>:
> Another good use of 'choice' and 'so' is in unit tests. In most
> languages we can write a suite of unit tests which give back booleans:
>
> double : Nat -> Nat
> double x = x + x
>
> doubleTwoTest : Bool
> doubleTwoTest = double 2 == 4
>
> In dependently typed languages like Idris we can go one step further and
> enforce these tests at compile-time:
>
> doubleTwoProof : so (double 2 == 4)
> doubleTwoProof = oh

BTW, there's a more straightforward way of doing such tests:

> doubleTwo : double 2 = 4
> doubleTwo = refl

This works the same and does not go through Bool.

Matus