Re: [racket-users] Learning by doing Typed Racket

[Konrad Hinsen]

On 13/06/2016 03:53, Daniel Prager wrote:


On Mon, Jun 13, 2016 at 10:59 AM, Matthew Butterick > wrote:

Some people, when confronted with a problem, think "I know, I'll use
Typed Racket."  Now they have (Pairof Problem Problem).


Most droll !

Taken seriously, when is the right time for TR vs Contracts vs lots of
tests vs whatever?


And, in the long run, for a synthesis. TR, contracts, and tests are all 
ways to formulate assertions about code. Today, it's the code authors 
who have to learn the subtleties of these different techniques and 
choose between them. I'd prefer to be able to write down all the 
assertions I can reasonably make about my code, and which I consider of 
use for human readers of my code, in a single place and notation, and 
let some program figure what which parts are best verified/enforced 
using which approach and at which time.


In my opinion, this is one main reason why so many programmers still 
prefer dynamic typing. They do see the advantages of having compilers 
perform checks, the more the better, but designing code with the 
idiosyncracies of the type-checkers-of-the-day as top priority isn't a 
very appealing approach.


Konrad.


--
You received this message because you are subscribed to the Google Groups "Racket 
Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] Learning by doing Typed Racket

[Ben Greenman]

On Sun, Jun 12, 2016 at 9:53 PM, Daniel Prager 
wrote:

> It seems that math libraries are a sweet-spot for TR. What else?
>
>
The math library has to deal with all the same growing pains (inst, assert).
I think part of the reason it looks so good is that it sparked improvements
in TR along the way.

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] Learning by doing Typed Racket

[Daniel Prager]

On Mon, Jun 13, 2016 at 10:59 AM, Matthew Butterick  wrote:

> Some people, when confronted with a problem, think "I know, I'll use Typed
> Racket."  Now they have (Pairof Problem Problem).
>
>
Most droll !

Taken seriously, when is the right time for TR vs Contracts vs lots of
tests vs whatever?

It seems that math libraries are a sweet-spot for TR. What else?


Dan

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] Learning by doing Typed Racket

[Matthias Felleisen]

> On Jun 12, 2016, at 8:59 PM, Matthew Butterick  wrote:
> 
> Now they have (Pairof Problem Problem).


:-)) [sorry for the bandwidth but this way cute]

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] Learning by doing Typed Racket

[Matthew Butterick]

Some people, when confronted with a problem, think "I know, I'll use Typed 
Racket."  Now they have (Pairof Problem Problem).


On Jun 12, 2016, at 2:29 PM, Ben Greenman  wrote:

> Yeah I agree `inst` needs more documentation.
> And as someone (Matthew B.?) suggested before, we could really use a 
> systematic way of documenting the type variables on each polymorphic function.
> 
> 
> On Sun, Jun 12, 2016 at 5:23 PM, Daniel Prager  
> wrote:
> Cc:ing the list ...
> 
> On Sun, Jun 12, 2016 at 4:56 PM, Ben Greenman  
> wrote:
> Yep, use `inst` to instantiate the polymorphic variables to sort.
> 
> #lang typed/racket
> 
> ((inst sort (List Symbol Integer) Integer)
>  '((a 45) (b 13) (c 12) (d 16) (e 9) (f 5)) < #:key second)
> 
> 
> [[ I usually start with `(inst f)` and use the error message to figure
> out what types / how many `f` needs. ]]
> 
> Thanks Ben, this is very helpful.
> 
> I had read about inst in the Racket Reference, but the penny hadn't dropped. 
> Perhaps expanding the worked example (or adding a section to The TR Guide) 
> would be helpful to novices.
> 
> For example:
> 
> > (foldl cons null (list 1 2 3 4)) 
> 
> Type Checker: Polymorphic function `foldl' could not be applied to arguments 
> [etc.]
> 
> Both foldl and cons are polymorphic: foldl in a b c d, cons in a b.
>  
> > foldl
> - : (All (a b c d)
>   (case->
>(-> (-> a b b) b (Listof a) b)
>(-> (-> a b c c) c (Listof a) (Listof b) c)
>(-> (-> a b c d d) d (Listof a) (Listof b) (Listof c) d)))
> #
> 
> > cons
> - : (All (a b) 
>   (case-> (-> a (Listof a) (Listof a)) 
>   (-> a b (Pairof a b
> #
> 
> The type-checker needs the programmer's help -- either by inst-antiating 
> foldl or cons -- to resolve this ambiguity. [Why?]:
> 
> > ((inst foldl Integer (Listof Integer) Null Null)
>cons null (list 1 2 3 4))
> - : (Listof Integer)
> '(4 3 2 1)
> 
> > (foldl (inst cons Integer Integer) null (list 1 2 3 4))
> - : (Listof Integer)
> '(4 3 2 1) 
> 
> In this case inst-ing cons is more concise than inst-ing foldl (in which the 
> Nulls are placeholders since c & d are ignored), so preferable.
> 
> * * *
> 
> Also, perhaps discoverability would be improved if the error message 
> suggested that an inst could resolve the problem.
> 
> Dan 
> 
> 
> On 6/11/16, Daniel Prager  wrote:
> > Next example.
> >
> > In Racket:
> >
> >> (sort '((a 45) (b 13) (c 12) (d 16) (e 9) (f 5)) < #:key second)
> >
> > '((f 5) (e 9) (c 12) (b 13) (d 16) (a 45))
> >
> >
> > In Typed Racket I couldn't get a version using #:key to type-check. Pulling
> > second into a comparison function works:
> >
> >> (sort '((a 45) (b 13) (c 12) (d 16) (e 9) (f 5))
> >   (λ ([a : (List Symbol Natural)]
> >   [b : (List Symbol Natural)])
> > (< (second a) (second b
> >
> > Is there a solution using #:key in Typed Racket?
> >
> >
> > Dan
> >
> > --
> > You received this message because you are subscribed to the Google Groups
> > "Racket Users" group.
> > To unsubscribe from this group and stop receiving emails from it, send an
> > email to racket-users+unsubscr...@googlegroups.com.
> > For more options, visit https://groups.google.com/d/optout.
> >
> 
> 
> --
> @ Northeastern University
> 
> 
> -- 
> You received this message because you are subscribed to the Google Groups 
> "Racket Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an 
> email to racket-users+unsubscr...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] Learning by doing Typed Racket

[Daniel Prager]

> we could really use a systematic way of documenting the type variables on
each polymorphic function.

That would be most welcome!

Dan

On Mon, Jun 13, 2016 at 7:29 AM, Ben Greenman 
wrote:

> Yeah I agree `inst` needs more documentation.
> And as someone (Matthew B.?) suggested before, we could really use a
> systematic way of documenting the type variables on each polymorphic
> function.
>
>
> On Sun, Jun 12, 2016 at 5:23 PM, Daniel Prager 
> wrote:
>
>> Cc:ing the list ...
>>
>> On Sun, Jun 12, 2016 at 4:56 PM, Ben Greenman <
>> benjaminlgreen...@gmail.com> wrote:
>>
>>> Yep, use `inst` to instantiate the polymorphic variables to sort.
>>>
>>> #lang typed/racket
>>>
>>> ((inst sort (List Symbol Integer) Integer)
>>>  '((a 45) (b 13) (c 12) (d 16) (e 9) (f 5)) < #:key second)
>>>
>>>
>>> [[ I usually start with `(inst f)` and use the error message to figure
>>> out what types / how many `f` needs. ]]
>>>
>>
>> Thanks Ben, this is very helpful.
>>
>> I had read about inst in the Racket Reference, but the penny hadn't
>> dropped. Perhaps expanding the worked example (or adding a section to The
>> TR Guide) would be helpful to novices.
>>
>> For example:
>>
>> > (foldl cons null (list 1 2 3 4))
>>
>> Type Checker: Polymorphic function `foldl' could not be applied to
>> arguments [etc.]
>>
>> Both foldl and cons are polymorphic: foldl in a b c d, cons in a b.
>>
>> > foldl
>> - : (All (a b c d)
>>   (case->
>>(-> (-> a b b) b (Listof a) b)
>>(-> (-> a b c c) c (Listof a) (Listof b) c)
>>(-> (-> a b c d d) d (Listof a) (Listof b) (Listof c) d)))
>> #
>>
>> > cons
>> - : (All (a b)
>>   (case-> (-> a (Listof a) (Listof a))
>>   (-> a b (Pairof a b
>> #
>>
>> The type-checker needs the programmer's help -- either by inst-antiating
>> foldl or cons -- to resolve this ambiguity. [Why?]:
>>
>> > ((inst foldl Integer (Listof Integer) Null Null)
>>cons null (list 1 2 3 4))
>> - : (Listof Integer)
>> '(4 3 2 1)
>>
>> > (foldl (inst cons Integer Integer) null (list 1 2 3 4))
>> - : (Listof Integer)
>> '(4 3 2 1)
>>
>> In this case inst-ing cons is more concise than inst-ing foldl (in which
>> the Nulls are placeholders since c & d are ignored), so preferable.
>>
>> * * *
>>
>> Also, perhaps discoverability would be improved if the error message
>> suggested that an inst could resolve the problem.
>>
>> Dan
>>
>>
>>> On 6/11/16, Daniel Prager  wrote:
>>> > Next example.
>>> >
>>> > In Racket:
>>> >
>>> >> (sort '((a 45) (b 13) (c 12) (d 16) (e 9) (f 5)) < #:key second)
>>> >
>>> > '((f 5) (e 9) (c 12) (b 13) (d 16) (a 45))
>>> >
>>> >
>>> > In Typed Racket I couldn't get a version using #:key to type-check.
>>> Pulling
>>> > second into a comparison function works:
>>> >
>>> >> (sort '((a 45) (b 13) (c 12) (d 16) (e 9) (f 5))
>>> >   (λ ([a : (List Symbol Natural)]
>>> >   [b : (List Symbol Natural)])
>>> > (< (second a) (second b
>>> >
>>> > Is there a solution using #:key in Typed Racket?
>>> >
>>> >
>>> > Dan
>>> >
>>> > --
>>> > You received this message because you are subscribed to the Google
>>> Groups
>>> > "Racket Users" group.
>>> > To unsubscribe from this group and stop receiving emails from it, send
>>> an
>>> > email to racket-users+unsubscr...@googlegroups.com.
>>> > For more options, visit https://groups.google.com/d/optout.
>>> >
>>>
>>>
>>> --
>>> @ Northeastern University
>>
>>
>


-- 
*Daniel Prager*
Agile/Lean Coaching, Innovation, and Leadership
Profile: skillfire.co/dan
Startups: youpatch.com , skillfire.co
Twitter: @agilejitsu 
Blog: agile-jitsu.blogspot.com
Linkedin: au.linkedin.com/in/danielaprager

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] Learning by doing Typed Racket

[Ben Greenman]

Yeah I agree `inst` needs more documentation.
And as someone (Matthew B.?) suggested before, we could really use a
systematic way of documenting the type variables on each polymorphic
function.


On Sun, Jun 12, 2016 at 5:23 PM, Daniel Prager 
wrote:

> Cc:ing the list ...
>
> On Sun, Jun 12, 2016 at 4:56 PM, Ben Greenman  > wrote:
>
>> Yep, use `inst` to instantiate the polymorphic variables to sort.
>>
>> #lang typed/racket
>>
>> ((inst sort (List Symbol Integer) Integer)
>>  '((a 45) (b 13) (c 12) (d 16) (e 9) (f 5)) < #:key second)
>>
>>
>> [[ I usually start with `(inst f)` and use the error message to figure
>> out what types / how many `f` needs. ]]
>>
>
> Thanks Ben, this is very helpful.
>
> I had read about inst in the Racket Reference, but the penny hadn't
> dropped. Perhaps expanding the worked example (or adding a section to The
> TR Guide) would be helpful to novices.
>
> For example:
>
> > (foldl cons null (list 1 2 3 4))
>
> Type Checker: Polymorphic function `foldl' could not be applied to
> arguments [etc.]
>
> Both foldl and cons are polymorphic: foldl in a b c d, cons in a b.
>
> > foldl
> - : (All (a b c d)
>   (case->
>(-> (-> a b b) b (Listof a) b)
>(-> (-> a b c c) c (Listof a) (Listof b) c)
>(-> (-> a b c d d) d (Listof a) (Listof b) (Listof c) d)))
> #
>
> > cons
> - : (All (a b)
>   (case-> (-> a (Listof a) (Listof a))
>   (-> a b (Pairof a b
> #
>
> The type-checker needs the programmer's help -- either by inst-antiating
> foldl or cons -- to resolve this ambiguity. [Why?]:
>
> > ((inst foldl Integer (Listof Integer) Null Null)
>cons null (list 1 2 3 4))
> - : (Listof Integer)
> '(4 3 2 1)
>
> > (foldl (inst cons Integer Integer) null (list 1 2 3 4))
> - : (Listof Integer)
> '(4 3 2 1)
>
> In this case inst-ing cons is more concise than inst-ing foldl (in which
> the Nulls are placeholders since c & d are ignored), so preferable.
>
> * * *
>
> Also, perhaps discoverability would be improved if the error message
> suggested that an inst could resolve the problem.
>
> Dan
>
>
>> On 6/11/16, Daniel Prager  wrote:
>> > Next example.
>> >
>> > In Racket:
>> >
>> >> (sort '((a 45) (b 13) (c 12) (d 16) (e 9) (f 5)) < #:key second)
>> >
>> > '((f 5) (e 9) (c 12) (b 13) (d 16) (a 45))
>> >
>> >
>> > In Typed Racket I couldn't get a version using #:key to type-check.
>> Pulling
>> > second into a comparison function works:
>> >
>> >> (sort '((a 45) (b 13) (c 12) (d 16) (e 9) (f 5))
>> >   (λ ([a : (List Symbol Natural)]
>> >   [b : (List Symbol Natural)])
>> > (< (second a) (second b
>> >
>> > Is there a solution using #:key in Typed Racket?
>> >
>> >
>> > Dan
>> >
>> > --
>> > You received this message because you are subscribed to the Google
>> Groups
>> > "Racket Users" group.
>> > To unsubscribe from this group and stop receiving emails from it, send
>> an
>> > email to racket-users+unsubscr...@googlegroups.com.
>> > For more options, visit https://groups.google.com/d/optout.
>> >
>>
>>
>> --
>> @ Northeastern University
>
>

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] Learning by doing Typed Racket

[Daniel Prager]

Cc:ing the list ...

On Sun, Jun 12, 2016 at 4:56 PM, Ben Greenman 
wrote:

> Yep, use `inst` to instantiate the polymorphic variables to sort.
>
> #lang typed/racket
>
> ((inst sort (List Symbol Integer) Integer)
>  '((a 45) (b 13) (c 12) (d 16) (e 9) (f 5)) < #:key second)
>
>
> [[ I usually start with `(inst f)` and use the error message to figure
> out what types / how many `f` needs. ]]
>

Thanks Ben, this is very helpful.

I had read about inst in the Racket Reference, but the penny hadn't
dropped. Perhaps expanding the worked example (or adding a section to The
TR Guide) would be helpful to novices.

For example:

> (foldl cons null (list 1 2 3 4))

Type Checker: Polymorphic function `foldl' could not be applied to
arguments [etc.]

Both foldl and cons are polymorphic: foldl in a b c d, cons in a b.

> foldl
- : (All (a b c d)
  (case->
   (-> (-> a b b) b (Listof a) b)
   (-> (-> a b c c) c (Listof a) (Listof b) c)
   (-> (-> a b c d d) d (Listof a) (Listof b) (Listof c) d)))
#

> cons
- : (All (a b)
  (case-> (-> a (Listof a) (Listof a))
  (-> a b (Pairof a b
#

The type-checker needs the programmer's help -- either by inst-antiating
foldl or cons -- to resolve this ambiguity. [Why?]:

> ((inst foldl Integer (Listof Integer) Null Null)
   cons null (list 1 2 3 4))
- : (Listof Integer)
'(4 3 2 1)

> (foldl (inst cons Integer Integer) null (list 1 2 3 4))
- : (Listof Integer)
'(4 3 2 1)

In this case inst-ing cons is more concise than inst-ing foldl (in which
the Nulls are placeholders since c & d are ignored), so preferable.

* * *

Also, perhaps discoverability would be improved if the error message
suggested that an inst could resolve the problem.

Dan


> On 6/11/16, Daniel Prager  wrote:
> > Next example.
> >
> > In Racket:
> >
> >> (sort '((a 45) (b 13) (c 12) (d 16) (e 9) (f 5)) < #:key second)
> >
> > '((f 5) (e 9) (c 12) (b 13) (d 16) (a 45))
> >
> >
> > In Typed Racket I couldn't get a version using #:key to type-check.
> Pulling
> > second into a comparison function works:
> >
> >> (sort '((a 45) (b 13) (c 12) (d 16) (e 9) (f 5))
> >   (λ ([a : (List Symbol Natural)]
> >   [b : (List Symbol Natural)])
> > (< (second a) (second b
> >
> > Is there a solution using #:key in Typed Racket?
> >
> >
> > Dan
> >
> > --
> > You received this message because you are subscribed to the Google Groups
> > "Racket Users" group.
> > To unsubscribe from this group and stop receiving emails from it, send an
> > email to racket-users+unsubscr...@googlegroups.com.
> > For more options, visit https://groups.google.com/d/optout.
> >
>
>
> --
> @ Northeastern University

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] Learning by doing Typed Racket

[Daniel Prager]

Next example.

In Racket:

> (sort '((a 45) (b 13) (c 12) (d 16) (e 9) (f 5)) < #:key second)

'((f 5) (e 9) (c 12) (b 13) (d 16) (a 45))


In Typed Racket I couldn't get a version using #:key to type-check. Pulling
second into a comparison function works:

> (sort '((a 45) (b 13) (c 12) (d 16) (e 9) (f 5))
  (λ ([a : (List Symbol Natural)]
  [b : (List Symbol Natural)])
(< (second a) (second b

Is there a solution using #:key in Typed Racket?


Dan

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] Learning by doing Typed Racket

[Ben Greenman]

Ah, okay. Well maybe try the Haskell or OCaml versions of the 99 problems?

https://wiki.haskell.org/H-99:_Ninety-Nine_Haskell_Problems
https://ocaml.org/learn/tutorials/99problems.html


On Sat, Jun 11, 2016 at 3:28 AM, Daniel Prager 
wrote:

> Hi Ben
>
> I wrote:
>
>> Do you have an alternative recommendation in mind?
>
>
> At that point I was asking whether Sam (or others) recommended another set
> of problems more conducive to learning Typed Racket than the 99 Lisp
> Problems which Sam said were a tricky place to start.
>
> I can see that staying clear of macros avoids an additional layer of
> sophistication.
>
> Dan
>
>
> On Sat, Jun 11, 2016 at 5:13 PM, Ben Greenman  > wrote:
>
>>
>> On Sat, Jun 11, 2016 at 12:46 AM, Daniel Prager <
>> daniel.a.pra...@gmail.com> wrote:
>>
>>> Do you have an alternative recommendation in mind?
>>
>>
>> I guess you already solved this one, but for later it might help to avoid
>> macros.
>>
>
>
>
> --
> *Daniel Prager*
> Agile/Lean Coaching, Innovation, and Leadership
> Profile: skillfire.co/dan
> Startups: youpatch.com , skillfire.co
> Twitter: @agilejitsu 
> Blog: agile-jitsu.blogspot.com
> Linkedin: au.linkedin.com/in/danielaprager
>

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] Learning by doing Typed Racket

[Ben Greenman]

On Sat, Jun 11, 2016 at 12:46 AM, Daniel Prager 
wrote:

> Do you have an alternative recommendation in mind?


I guess you already solved this one, but for later it might help to avoid
macros.

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] Learning by doing Typed Racket

[Daniel Prager]

Ok, it took me a while to see how to eliminate the apply:

(define-syntax-rule (table (a ...) body)
  (for/list : (Listof (Listof Boolean))
([b : (Listof Boolean) (boolean-tuple (length '(a ...)))])
(match-define (list a ...) b)
(append b (list ((λ ([a : Boolean] ...) : Boolean
   body) a ...)


Dan

On Sat, Jun 11, 2016 at 7:47 AM, Sam Tobin-Hochstadt 
wrote:

> The problem here is that you have a fixed-argument function (taking 3
> Boolean arguments) and you're applying it to a list of unknown length. Your
> program knows that this won't be a problem, because `boolean-tuple` always
> produces a list of exactly the right length, but Typed Racket doesn't know
> that.
>
> Sam
>
> On Fri, Jun 10, 2016 at 5:39 PM Daniel Prager 
> wrote:
>
>> I'm working my way through the 99 Lisp Problems (
>> http://www.ic.unicamp.br/~meidanis/courses/mc336/2006s2/funcional/L-99_Ninety-Nine_Lisp_Problems.html)
>> to improve my proficiency with Typed Racket.
>>
>> While sometimes the discipline of the types helps me catch mistakes,
>> quite often I find myself wrestling to get through the type-check.
>>
>> My tactics to get things working include: dropping back to Racket to make
>> the program work first, switching between for/... and recursive forms,
>> widening the type (e.g. from Natural to Integer), and using cast.
>>
>> I'll post some examples of where I've struggled (or am struggling). First
>> example below.
>>
>> Tips and strategies gratefully accepted!
>>
>> Dan
>>
>>
>> The first example writes out truth tables for a boolean expression with
>> an arbitrary number of parameters.
>>
>> E.g.
>>
>> > (table (a b c) (equal? (and a (or b c))
>>  (or (and a b)
>>  (and a c
>> ;  a  b  c  result
>> ;
>> '((#t #t #t #t)
>>   (#t #t #f #t)
>>   (#t #f #t #t)
>>   (#t #f #f #t)
>>   (#f #t #t #t)
>>   (#f #t #f #t)
>>   (#f #f #t #t)
>>   (#f #f #f #t))
>>
>>
>> Works in Racket:
>>
>> #lang racket
>>
>> ;P48 (**) Truth tables for logical expressions (3).
>>
>> (define (boolean-tuple n)
>>   (if (= n 1)
>>   '((#t) (#f))
>>   (for*/list
>> ([a '(#t #f)] [t (boolean-tuple (sub1 n))])
>> (cons a t
>>
>> (define-syntax-rule (table (a ...) body)
>>   (for/list
>> ([b (boolean-tuple (length '(a ...)))])
>> (append b (list (apply (λ (a ...)
>>  body)
>>b)
>>
>>
>> Can't get past type-check in TR:
>>
>> #lang typed/racket
>>
>>
>> (define (boolean-tuple [n : Integer]) : (Listof (Listof Boolean))
>>   (if (= n 1)
>>   '((#t) (#f))
>>   (for*/list : (Listof (Listof Boolean))
>> ([a '(#t #f)] [t (boolean-tuple (sub1 n))])
>> (cons a t
>>
>> (define-syntax-rule (table (a ...) body)
>>   (for/list : (Listof (Listof Boolean))
>> ([b : (Listof Boolean) (boolean-tuple (length '(a ...)))])
>> (append b (list (apply (λ ([a : Boolean] ...) : Boolean
>>  body)
>>b)
>>
>> Type Checker: Bad arguments to function in `apply':
>> Domain: Boolean Boolean Boolean
>> Arguments: (Listof Boolean) *
>>  in: (apply (λ ((a : Boolean) ...) : Boolean body) b)
>>
>> --
>> You received this message because you are subscribed to the Google Groups
>> "Racket Users" group.
>> To unsubscribe from this group and stop receiving emails from it, send an
>> email to racket-users+unsubscr...@googlegroups.com.
>> For more options, visit https://groups.google.com/d/optout.
>>
>


-- 
*Daniel Prager*
Agile/Lean Coaching, Innovation, and Leadership
Profile: skillfire.co/dan
Startups: youpatch.com , skillfire.co
Twitter: @agilejitsu 
Blog: agile-jitsu.blogspot.com
Linkedin: au.linkedin.com/in/danielaprager

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] Learning by doing Typed Racket

[Daniel Prager]

On Sat, Jun 11, 2016 at 8:17 AM, Sam Tobin-Hochstadt 
wrote:

> The easiest way to avoid this is to program with the types, and the
> type checker, in mind from the start.


That's what I'm trying to do, hampered by my limited of understanding of
the limits of the type-checker (Robby's point).


> If you write a maximally-clever Racket program, and then try to get it to
> type check, you will
> probably need to change it.
>

I'll take that as a back-handed compliment! ;-)

For these problems I'm starting in Typed Racket and dropping back to Racket
when I get stuck, and not *trying* to be clever, just trying to solve the
problems.

E.g. I'm not sure how I would solve this one with less cleverness, given an
objective of being able to execute expressions of the form (table (a b c)
etc.) with an arbitrary number of variables.


> Also, I expect that those problems in particular seem to involve a lot
> of punning back and forth between lists as sequences and lists as
> fixed-length data, which is the sort of traditional lisp & scheme
> style that is unlikely to work well in Typed Racket.


The nature of the problems may be the source of the difficulty, but I'm
also running into similar difficulties with the number-theory type problems.

So that might not be the best place to start.
>

Do you have an alternative recommendation in mind?


Dan

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] Learning by doing Typed Racket

[Robby Findler]

On Fri, Jun 10, 2016 at 5:17 PM, Sam Tobin-Hochstadt
 wrote:
> The easiest way to avoid this is to program with the types, and the
> type checker, in mind from the start. If you write a maximally-clever
> Racket program, and then try to get it to type check, you will
> probably need to change it.

This is probably good advice only to people who already understand the
type checker and not people that are trying programming problems to
learn how the type checker thinks.

Robby

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] Learning by doing Typed Racket

[Sam Tobin-Hochstadt]

The easiest way to avoid this is to program with the types, and the
type checker, in mind from the start. If you write a maximally-clever
Racket program, and then try to get it to type check, you will
probably need to change it.

Also, I expect that those problems in particular seem to involve a lot
of punning back and forth between lists as sequences and lists as
fixed-length data, which is the sort of traditional lisp & scheme
style that is unlikely to work well in Typed Racket. So that might not
be the best place to start.

Sam

On Fri, Jun 10, 2016 at 6:09 PM, Daniel Prager
 wrote:
> Thanks Sam
>
> I seem to repeatedly come up against this sort of problem, where I can make
> inferences that are beyond the ken of Typed Racket.
>
> Do you have general advice, given TR's "by design" conservatism?
>
> Dan
>
>
> On Sat, Jun 11, 2016 at 7:47 AM, Sam Tobin-Hochstadt 
> wrote:
>>
>> The problem here is that you have a fixed-argument function (taking 3
>> Boolean arguments) and you're applying it to a list of unknown length. Your
>> program knows that this won't be a problem, because `boolean-tuple` always
>> produces a list of exactly the right length, but Typed Racket doesn't know
>> that.
>>
>> Sam
>>
>> On Fri, Jun 10, 2016 at 5:39 PM Daniel Prager 
>> wrote:
>>>
>>> I'm working my way through the 99 Lisp Problems
>>> (http://www.ic.unicamp.br/~meidanis/courses/mc336/2006s2/funcional/L-99_Ninety-Nine_Lisp_Problems.html)
>>> to improve my proficiency with Typed Racket.
>>>
>>> While sometimes the discipline of the types helps me catch mistakes,
>>> quite often I find myself wrestling to get through the type-check.
>>>
>>> My tactics to get things working include: dropping back to Racket to make
>>> the program work first, switching between for/... and recursive forms,
>>> widening the type (e.g. from Natural to Integer), and using cast.
>>>
>>> I'll post some examples of where I've struggled (or am struggling). First
>>> example below.
>>>
>>> Tips and strategies gratefully accepted!
>>>
>>> Dan
>>>
>>>
>>> The first example writes out truth tables for a boolean expression with
>>> an arbitrary number of parameters.
>>>
>>> E.g.
>>>
>>> > (table (a b c) (equal? (and a (or b c))
>>>  (or (and a b)
>>>  (and a c
>>> ;  a  b  c  result
>>> ;
>>> '((#t #t #t #t)
>>>   (#t #t #f #t)
>>>   (#t #f #t #t)
>>>   (#t #f #f #t)
>>>   (#f #t #t #t)
>>>   (#f #t #f #t)
>>>   (#f #f #t #t)
>>>   (#f #f #f #t))
>>>
>>>
>>> Works in Racket:
>>>
>>> #lang racket
>>>
>>> ;P48 (**) Truth tables for logical expressions (3).
>>>
>>> (define (boolean-tuple n)
>>>   (if (= n 1)
>>>   '((#t) (#f))
>>>   (for*/list
>>> ([a '(#t #f)] [t (boolean-tuple (sub1 n))])
>>> (cons a t
>>>
>>> (define-syntax-rule (table (a ...) body)
>>>   (for/list
>>> ([b (boolean-tuple (length '(a ...)))])
>>> (append b (list (apply (λ (a ...)
>>>  body)
>>>b)
>>>
>>>
>>> Can't get past type-check in TR:
>>>
>>> #lang typed/racket
>>>
>>>
>>> (define (boolean-tuple [n : Integer]) : (Listof (Listof Boolean))
>>>   (if (= n 1)
>>>   '((#t) (#f))
>>>   (for*/list : (Listof (Listof Boolean))
>>> ([a '(#t #f)] [t (boolean-tuple (sub1 n))])
>>> (cons a t
>>>
>>> (define-syntax-rule (table (a ...) body)
>>>   (for/list : (Listof (Listof Boolean))
>>> ([b : (Listof Boolean) (boolean-tuple (length '(a ...)))])
>>> (append b (list (apply (λ ([a : Boolean] ...) : Boolean
>>>  body)
>>>b)
>>>
>>> Type Checker: Bad arguments to function in `apply':
>>> Domain: Boolean Boolean Boolean
>>> Arguments: (Listof Boolean) *
>>>  in: (apply (λ ((a : Boolean) ...) : Boolean body) b)
>>>
>>> --
>>> You received this message because you are subscribed to the Google Groups
>>> "Racket Users" group.
>>> To unsubscribe from this group and stop receiving emails from it, send an
>>> email to racket-users+unsubscr...@googlegroups.com.
>>> For more options, visit https://groups.google.com/d/optout.
>
>
>
>
> --
> Daniel Prager
> Agile/Lean Coaching, Innovation, and Leadership
> Profile: skillfire.co/dan
> Startups: youpatch.com, skillfire.co
> Twitter: @agilejitsu
> Blog: agile-jitsu.blogspot.com
> Linkedin: au.linkedin.com/in/danielaprager

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] Learning by doing Typed Racket

[Daniel Prager]

Thanks Sam

I seem to repeatedly come up against this sort of problem, where I can make
inferences that are beyond the ken of Typed Racket.

Do you have general advice, given TR's "by design" conservatism?

Dan


On Sat, Jun 11, 2016 at 7:47 AM, Sam Tobin-Hochstadt 
wrote:

> The problem here is that you have a fixed-argument function (taking 3
> Boolean arguments) and you're applying it to a list of unknown length. Your
> program knows that this won't be a problem, because `boolean-tuple` always
> produces a list of exactly the right length, but Typed Racket doesn't know
> that.
>
> Sam
>
> On Fri, Jun 10, 2016 at 5:39 PM Daniel Prager 
> wrote:
>
>> I'm working my way through the 99 Lisp Problems (
>> http://www.ic.unicamp.br/~meidanis/courses/mc336/2006s2/funcional/L-99_Ninety-Nine_Lisp_Problems.html)
>> to improve my proficiency with Typed Racket.
>>
>> While sometimes the discipline of the types helps me catch mistakes,
>> quite often I find myself wrestling to get through the type-check.
>>
>> My tactics to get things working include: dropping back to Racket to make
>> the program work first, switching between for/... and recursive forms,
>> widening the type (e.g. from Natural to Integer), and using cast.
>>
>> I'll post some examples of where I've struggled (or am struggling). First
>> example below.
>>
>> Tips and strategies gratefully accepted!
>>
>> Dan
>>
>>
>> The first example writes out truth tables for a boolean expression with
>> an arbitrary number of parameters.
>>
>> E.g.
>>
>> > (table (a b c) (equal? (and a (or b c))
>>  (or (and a b)
>>  (and a c
>> ;  a  b  c  result
>> ;
>> '((#t #t #t #t)
>>   (#t #t #f #t)
>>   (#t #f #t #t)
>>   (#t #f #f #t)
>>   (#f #t #t #t)
>>   (#f #t #f #t)
>>   (#f #f #t #t)
>>   (#f #f #f #t))
>>
>>
>> Works in Racket:
>>
>> #lang racket
>>
>> ;P48 (**) Truth tables for logical expressions (3).
>>
>> (define (boolean-tuple n)
>>   (if (= n 1)
>>   '((#t) (#f))
>>   (for*/list
>> ([a '(#t #f)] [t (boolean-tuple (sub1 n))])
>> (cons a t
>>
>> (define-syntax-rule (table (a ...) body)
>>   (for/list
>> ([b (boolean-tuple (length '(a ...)))])
>> (append b (list (apply (λ (a ...)
>>  body)
>>b)
>>
>>
>> Can't get past type-check in TR:
>>
>> #lang typed/racket
>>
>>
>> (define (boolean-tuple [n : Integer]) : (Listof (Listof Boolean))
>>   (if (= n 1)
>>   '((#t) (#f))
>>   (for*/list : (Listof (Listof Boolean))
>> ([a '(#t #f)] [t (boolean-tuple (sub1 n))])
>> (cons a t
>>
>> (define-syntax-rule (table (a ...) body)
>>   (for/list : (Listof (Listof Boolean))
>> ([b : (Listof Boolean) (boolean-tuple (length '(a ...)))])
>> (append b (list (apply (λ ([a : Boolean] ...) : Boolean
>>  body)
>>b)
>>
>> Type Checker: Bad arguments to function in `apply':
>> Domain: Boolean Boolean Boolean
>> Arguments: (Listof Boolean) *
>>  in: (apply (λ ((a : Boolean) ...) : Boolean body) b)
>>
>> --
>> You received this message because you are subscribed to the Google Groups
>> "Racket Users" group.
>> To unsubscribe from this group and stop receiving emails from it, send an
>> email to racket-users+unsubscr...@googlegroups.com.
>> For more options, visit https://groups.google.com/d/optout.
>>
>


-- 
*Daniel Prager*
Agile/Lean Coaching, Innovation, and Leadership
Profile: skillfire.co/dan
Startups: youpatch.com , skillfire.co
Twitter: @agilejitsu 
Blog: agile-jitsu.blogspot.com
Linkedin: au.linkedin.com/in/danielaprager

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] Learning by doing Typed Racket

[Sam Tobin-Hochstadt]

The problem here is that you have a fixed-argument function (taking 3
Boolean arguments) and you're applying it to a list of unknown length. Your
program knows that this won't be a problem, because `boolean-tuple` always
produces a list of exactly the right length, but Typed Racket doesn't know
that.

Sam

On Fri, Jun 10, 2016 at 5:39 PM Daniel Prager 
wrote:

> I'm working my way through the 99 Lisp Problems (
> http://www.ic.unicamp.br/~meidanis/courses/mc336/2006s2/funcional/L-99_Ninety-Nine_Lisp_Problems.html)
> to improve my proficiency with Typed Racket.
>
> While sometimes the discipline of the types helps me catch mistakes, quite
> often I find myself wrestling to get through the type-check.
>
> My tactics to get things working include: dropping back to Racket to make
> the program work first, switching between for/... and recursive forms,
> widening the type (e.g. from Natural to Integer), and using cast.
>
> I'll post some examples of where I've struggled (or am struggling). First
> example below.
>
> Tips and strategies gratefully accepted!
>
> Dan
>
>
> The first example writes out truth tables for a boolean expression with an
> arbitrary number of parameters.
>
> E.g.
>
> > (table (a b c) (equal? (and a (or b c))
>  (or (and a b)
>  (and a c
> ;  a  b  c  result
> ;
> '((#t #t #t #t)
>   (#t #t #f #t)
>   (#t #f #t #t)
>   (#t #f #f #t)
>   (#f #t #t #t)
>   (#f #t #f #t)
>   (#f #f #t #t)
>   (#f #f #f #t))
>
>
> Works in Racket:
>
> #lang racket
>
> ;P48 (**) Truth tables for logical expressions (3).
>
> (define (boolean-tuple n)
>   (if (= n 1)
>   '((#t) (#f))
>   (for*/list
> ([a '(#t #f)] [t (boolean-tuple (sub1 n))])
> (cons a t
>
> (define-syntax-rule (table (a ...) body)
>   (for/list
> ([b (boolean-tuple (length '(a ...)))])
> (append b (list (apply (λ (a ...)
>  body)
>b)
>
>
> Can't get past type-check in TR:
>
> #lang typed/racket
>
>
> (define (boolean-tuple [n : Integer]) : (Listof (Listof Boolean))
>   (if (= n 1)
>   '((#t) (#f))
>   (for*/list : (Listof (Listof Boolean))
> ([a '(#t #f)] [t (boolean-tuple (sub1 n))])
> (cons a t
>
> (define-syntax-rule (table (a ...) body)
>   (for/list : (Listof (Listof Boolean))
> ([b : (Listof Boolean) (boolean-tuple (length '(a ...)))])
> (append b (list (apply (λ ([a : Boolean] ...) : Boolean
>  body)
>b)
>
> Type Checker: Bad arguments to function in `apply':
> Domain: Boolean Boolean Boolean
> Arguments: (Listof Boolean) *
>  in: (apply (λ ((a : Boolean) ...) : Boolean body) b)
>
> --
> You received this message because you are subscribed to the Google Groups
> "Racket Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to racket-users+unsubscr...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
>

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.