badkins
2020-8-4 14:36:48

I can’t help with the typing issue (I’m primarily a dynamic typer), but thanks for the example because it exposed a gap in my understanding of match - I really need to dig into the match grammar more!


samth
2020-8-4 16:08:29

Unfortunately that looks like a weakness in Typed Racket


samth
2020-8-4 16:08:38

Can you file a bug report?


noahstorym
2020-8-4 16:30:13

Yes, I have reported it: https://github.com/racket/typed-racket/issues/956


samth
2020-8-4 18:59:54

Thanks!


noahstorym
2020-8-5 01:51:05

I found some strange behavior of recursive type in typed/racket.

Following codes work well: #lang typed/racket (define-type Func (All (A) [-> Boolean Number Any A])) (: test-func [-> Number Number]) (define test-func (λ (num) ((λ (func) num) (λ ([func : Func]) (inst func Number))))) #lang typed/racket (define-type Func (All (A) [-> Func A])) (: test-func [-> Number Number]) (define test-func (λ (num) ((λ (func) num) (λ ([func : (Func Number)]) func)))) run test-func (test-func 0) ; -> 0 (test-func 1) ; -> 1 (test-func 2) ; -> 2 (test-func 3) ; -> 3 (test-func 4) ; -> 4 But this code failed: #lang typed/racket (define-type Func (All (A) [-> Func A])) (: test-func [-> Number Number]) (define test-func (λ (num) ((λ (func) num) (λ ([func : Func]) (inst func Number))))) error message: Type Checker: Cannot instantiate non-polymorphic type Func in: func


noahstorym
2020-8-5 01:51:36

Here is another problem about recursive type:

Following code failed: #lang typed/racket (define-type Func (All (A) [-> Func A])) (: test-func-2 [-> Number Number]) (define test-func-2 (λ (arg) ((λ ([func-1 : Func]) arg) (λ ([func-2 : Func]) (func-2 func-2))))) error message: Type Checker: type mismatch expected: Func given: (-> Func Nothing) in: (λ ((func-2 : Func)) (func-2 func-2)) In fact, I’m also not sure what the type of (func-2 func-2) should be (maybe Nothing is right). But I don’t understand how racket infers Nothing .


yilin.wei10
2020-8-5 02:11:11

@yilin.wei10 has joined the channel


samth
2020-8-5 02:39:00

It chose Nothing because there were no constraints on the type argument


noahstorym
2020-8-5 02:49:25

I get it, thank you!


me1884
2020-8-5 04:09:01

@me1884 has joined the channel


maueroats
2020-8-5 04:16:16

I thought Any would be the type with no constraints? Nothing is a weird type, not even Void? It looks like Nothing is a type used when the function cannot return. I found this example in the passing tests to be humorous (and illustrative): (: h (-> Nothing)) (define (h) (h))


sorawee
2020-8-5 04:17:40

Well, this also works: (: h (-> Integer))


sorawee
2020-8-5 04:17:51

And pretty much anything putting there


noahstorym
2020-8-5 04:52:58

I think Nothing could be used to construct empty data structure. (define-type Null (Listof Nothing)) or as some special functions’ return type (for example, error and raise )

But I’m not sure what more Nothing can do.