KataBankOCR

503 views
Skip to first unread message

Paul Snively

unread,
Sep 21, 2012, 9:57:48 AM9/21/12
to shapel...@googlegroups.com
Hi everyone.

I have a presentation coming up at StrangeLoop, and I'm trying to work through the KataBankOCR found at http://codingdojo.org/cgi-bin/wiki.pl?KataBankOCR. It seems to me that Shapeless should be able to demonstrate some interesting points about the use of types in a rich type system like Scala's, but I haven't been able to work out exactly how. For example, I'd love to be able to tackle user story 2, and my thought about how this might go using Shapeless goes something like this:

  1. Define vals for each of the "OCR digits" comprising pipes, underscores, and spaces.
  2. Thanks to Scala's singleton types, each of those vals has a distinct type: zero.type, one.type, etc.
  3. Shapeless also gives me type-level Nats.
  4. Typeable gives me a cast that returns None on failure.
  5. I have the mother of all Scala HLists.
  6. I have Sized types.
So it seems like I should be able to define the type "9-element HList of Nats 0-9 such that their checksum modulo 11 is 0," and use Typeable to cast() a List[Int] to it. If I get Some, I have a valid value; if I get None, I don't.

Doable? Or have I found a limit? :-)

Miles Sabin

unread,
Sep 21, 2012, 10:19:03 AM9/21/12
to shapel...@googlegroups.com
On Fri, Sep 21, 2012 at 2:57 PM, Paul Snively <paulfs...@gmail.com> wrote:
> So it seems like I should be able to define the type "9-element HList of
> Nats 0-9 such that their checksum modulo 11 is 0," and use Typeable to
> cast() a List[Int] to it. If I get Some, I have a valid value; if I get
> None, I don't.
>
> Doable? Or have I found a limit? :-)

I think doable, although my gut feeling is that a compile time proof
that the sum of nine Nat's modulo 11 is equal to zero would be
painfully slow with the current encoding.

I wish I had some time to look at it, but unfortunately not right now
... any takers?

Cheers,


Miles

--
Miles Sabin
tel: +44 7813 944 528
skype: milessabin
gtalk: mi...@milessabin.com
g+: http://www.milessabin.com
http://twitter.com/milessabin

Paul Snively

unread,
Sep 21, 2012, 12:03:44 PM9/21/12
to shapel...@googlegroups.com
Hi Miles!


I think doable, although my gut feeling is that a compile time proof
that the sum of nine Nat's modulo 11 is equal to zero would be
painfully slow with the current encoding.

It's worse than that: the actual checksum, given an x: Int, is x.toString.reverse.zipWithIndex.foldLeft(0)((acc, pair) => acc + (pair._1.toString.toInt * (pair._2 + 1))), i.e. the sum of each digit * its-index-from-the-right-plus-1. That's principally why I thought it might be an insurmountable challenge to encode.
 
I wish I had some time to look at it, but unfortunately not right now
... any takers?

Any chance you could take a swipe at it before Monday? :-) I'll keep poking at it too, as well as trying to come up with other examples. 
 
Cheers,


Miles

--
Miles Sabin
tel: +44 7813 944 528
skype: milessabin
gtalk: mi...@milessabin.com
g+: http://www.milessabin.com
http://twitter.com/milessabin

Thanks so much!
Paul 

Miles Sabin

unread,
Sep 21, 2012, 12:17:56 PM9/21/12
to shapel...@googlegroups.com
On Fri, Sep 21, 2012 at 5:03 PM, Paul Snively <paulfs...@gmail.com> wrote:
> Any chance you could take a swipe at it before Monday? :-) I'll keep poking
> at it too, as well as trying to come up with other examples.

No chance at all I'm afraid ...

Paul Snively

unread,
Sep 21, 2012, 2:04:58 PM9/21/12
to shapel...@googlegroups.com

On Friday, September 21, 2012 9:18:28 AM UTC-7, Miles Sabin wrote:
No chance at all I'm afraid ...

Ah well, I had to ask. I'll keep digging. Thanks!

Travis Brown

unread,
Sep 21, 2012, 2:17:58 PM9/21/12
to shapel...@googlegroups.com
Hi Paul,

I think this does what you want, no?

https://gist.github.com/3763016

This compiles:

isValid(_3 :: _4 :: _5 :: _8 :: _8 :: _2 :: _8 :: _6 :: _5 :: HNil)

But these don't, for example:

isValid(_3 :: _1 :: _5 :: _8 :: _8 :: _2 :: _8 :: _6 :: _5 :: HNil)
isValid(_3 :: _4 :: _5 :: _8 :: _8 :: _2 :: _8 :: _6 :: HNil)

It is slow, but not as bad as I expected—on my machine it takes the compiler about 5 seconds to make up its mind.

Travis

Paul Snively

unread,
Sep 21, 2012, 3:18:21 PM9/21/12
to shapel...@googlegroups.com
Travis,

Wow, that's awesome! I was just trying to express some types and using Typeable to see if they satisfy the specifications, and running into trouble right away. Maybe you can also shed some light on this?


I guess it's a bit much to expect the _ to be inferred to be the type of the Nat I'm trying to cast, but it's not clear to me what the correct alternative is.

Ultimately, of course, what I really want is, given a list of the characters formed with pipes, underscores, and spaces, to be able to say cast[AccountNumber](scan) and get an Option[Int], iff it's a valid scan. It looks like your implementation gets me 99% of the way there. Thanks again!

Miles Sabin

unread,
Sep 21, 2012, 4:48:13 PM9/21/12
to shapel...@googlegroups.com
On Fri, Sep 21, 2012 at 7:17 PM, Travis Brown
<travisro...@gmail.com> wrote:
> I think this does what you want, no?
>
> https://gist.github.com/3763016
>
> This compiles:
>
> isValid(_3 :: _4 :: _5 :: _8 :: _8 :: _2 :: _8 :: _6 :: _5 :: HNil)
>
>
> But these don't, for example:
>
> isValid(_3 :: _1 :: _5 :: _8 :: _8 :: _2 :: _8 :: _6 :: _5 :: HNil)
>
> isValid(_3 :: _4 :: _5 :: _8 :: _8 :: _2 :: _8 :: _6 :: HNil)
>
>
> It is slow, but not as bad as I expected—on my machine it takes the compiler
> about 5 seconds to make up its mind.

Niiiice ... :-)

Travis Brown

unread,
Sep 22, 2012, 8:14:34 AM9/22/12
to shapel...@googlegroups.com
Hi Paul,

I'm not sure I understand the first part of what you're trying to do—getting an appropriately typed HList of Nats from a list of characters sounds tricky.

In your code snippet, Digit is a type class, so you can write the following, for example:

    val digitInstance = implicitly[Digit[_3]]

Or:

    def foo[N <: Nat: Digit](n: N) = n // Now foo(_11) won't compile, but foo(_3) will.

But it's not the case that the value _3 is a Digit in the sense that would be necessary for casting with Typeable.

Travis

Paul Snively

unread,
Sep 27, 2012, 6:09:01 PM9/27/12
to shapel...@googlegroups.com
Hi Travis,

On Saturday, September 22, 2012 5:14:35 AM UTC-7, Travis Brown wrote:
I'm not sure I understand the first part of what you're trying to do—getting an appropriately typed HList of Nats from a list of characters sounds tricky.
... 
But it's not the case that the value _3 is a Digit in the sense that would be necessary for casting with Typeable.

Upon reflection (no pun intended), you're obviously correct. So what I think I'm looking for is just a constructor from, say, an HList of Digits without the checksum constraint. This isn't a really good example, because there are zero cases where I'm interested in literal construction of such an account number, so maybe I should just move on and think of better examples. :-)

In any case, thanks for all your help! I used your implementation, with attribution of course, in a presentation at Strange Loop 2012 with Amanda Laucher. I'll post a link to the video when it's available. 
 
Travis

Best regards,
Paul 

Miles Sabin

unread,
Sep 27, 2012, 6:27:54 PM9/27/12
to shapel...@googlegroups.com
On Thu, Sep 27, 2012 at 11:09 PM, Paul Snively <paulfs...@gmail.com> wrote:
> In any case, thanks for all your help! I used your implementation, with
> attribution of course, in a presentation at Strange Loop 2012 with Amanda
> Laucher. I'll post a link to the video when it's available.

I'd like to see that. What was the reaction to the scary type-level madness?

Travis Brown

unread,
Sep 27, 2012, 10:19:23 PM9/27/12
to shapel...@googlegroups.com
Thanks, Paul! I'll look forward to seeing the video, and to hearing about reactions—

Travis

Jason Scott

unread,
Sep 16, 2014, 3:31:10 AM9/16/14
to shapel...@googlegroups.com
I've recently tried to follow along and implement this... some slight changes for shapeless 2.0.


However - it won't compile in eclipse (scala ide) nor in SBT with scala 2.11.2. I shouldn't say it "won't" compile - it tries "forever" and hangs....

As soon as I un-comment the two lines at the bottom which perform the isValid test eclipse hangs (and I have to destroy the whole project to get it back). SBT also hangs.

Any ideas?

Travis Brown

unread,
Sep 16, 2014, 11:12:15 AM9/16/14
to shapel...@googlegroups.com
Hi Jason!

The issue here is that for some reason 2.11 takes much, much longer than 2.10 to conjure up `Sum` instances, particularly if the first addend is large.

A little trick I've discovered in the two years since I wrote that code is that it's a good idea to put the addend that tends to be larger second. In this case `TS` is at most 10, while `HP` is potentially much larger. Since addition is commutative you can switch them freely, and changing that one line to `hs: Sum.Aux[TS, HP, HS]` makes the tests compile (or fail to compile) in a reasonable amount of time on my machine.

Travis
Message has been deleted

Jason Scott

unread,
Sep 16, 2014, 9:07:42 PM9/16/14
to shapel...@googlegroups.com
Thanks for that Travis - indeed it did fix the issue.

So by the looks of it Scala is immature for this type of type-level programming. After playing with the code for some time I still don't fully understand it anyway.   ;-)
Reply all
Reply to author
Forward
0 new messages