How to set type signature for recursive lazy list

[Kiong-Gē Liāu]

Hi, in non-typed racket, I can define a generalized Fibonacci sequence 

X[n+k] = f(X[n], X[n+1], ...., X[n+k-1])

using the following code 

#lang racket

(require  racket/stream)

(define (gfib f xs)

  (define (gfib_t xs)

    (stream-cons (last xs) (gfib_t (append (cdr xs) (list (f xs)))))) 

  (stream-append (drop-right xs 1) (gfib_t xs)))

(define (sum xs) (apply + xs))

;; Example of a (0, 1) initialized Fibonacci sequence 

(define gfib20 (gfib sum '(0 1 )))

But using typed racket,  the following code 

#lang typed/racket

(require pfds/stream)

(define (sum [xs : (Listof Number)] ) (apply + xs))

(define (gfib [f : (-> (Listof Number) Number)]  [xs : (Listof Number)] )

  (define (gfib_t [ys : (Listof Number)] )  

    (stream-cons (last ys) (gfib_t (append (cdr ys) (list (f ys))))))

  (stream-append (stream (drop-right xs 1)) (gfib_t xs)))

leads to error message 

; /home/kiong-ge/Programming/Racket/typed_racket_test.rkt:8:11: Type Checker: insufficient type information to typecheck. please add more type annotations

;   in: gfib_t

How should I set the type signature in the typed racket in order to get the same result generated non-typed racket code ?

Thanks, 

Kiong-Ge. 

[Shu-Hung You]

On Sun, Jul 11, 2021 at 8:15 PM Kiong-Gē Liāu <gongy...@gmail.com> wrote:
>
> Hi, in non-typed racket, I can define a generalized Fibonacci sequence
>
> X[n+k] = f(X[n], X[n+1], ...., X[n+k-1])
>
> using the following code
>
> #lang racket
>
> (require racket/stream)
>
> (define (gfib f xs)
> (define (gfib_t xs)
> (stream-cons (last xs) (gfib_t (append (cdr xs) (list (f xs))))))
> (stream-append (drop-right xs 1) (gfib_t xs)))
>
> (define (sum xs) (apply + xs))
> ;; Example of a (0, 1) initialized Fibonacci sequence
> (define gfib20 (gfib sum '(0 1 )))
>
> But using typed racket, the following code
>
> #lang typed/racket
>
> (require pfds/stream)
>
> (define (sum [xs : (Listof Number)] ) (apply + xs))
>
> (define (gfib [f : (-> (Listof Number) Number)] [xs : (Listof Number)] )
> (define (gfib_t [ys : (Listof Number)] )

^~~~~~~ You can annotate the codomain type of gfib_t here:

(define (gfib_t [ys : (Listof Number)]) : Your-Codomain-Type
...)

> (stream-cons (last ys) (gfib_t (append (cdr ys) (list (f ys))))))
> (stream-append (stream (drop-right xs 1)) (gfib_t xs)))
>
> leads to error message
>
> ; /home/kiong-ge/Programming/Racket/typed_racket_test.rkt:8:11: Type Checker: insufficient type information to typecheck. please add more type annotations
> ; in: gfib_t
>
> How should I set the type signature in the typed racket in order to get the same result generated non-typed racket code ?
>
> Thanks,
> Kiong-Ge.
>
>
>

> --
> 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...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/baa0af81-f7fb-46bf-b508-d35727cbaef2n%40googlegroups.com.

[Ben Greenman]

First, gfib_t needs a return type annotation. You can either add `:
(Stream Number)` to the end of the line, or write a full signature
above the define

(: gfib_t (-> (Listof Number) (Stream Number)))
(define (gfib_t ys)

After this, the typechecker can run. But it finds a problem with
stream-append. The issue here is that the two arguments to
stream-append have different types. One contains lists of numbers and
the other contains numbers.

typed.rkt:11:2: Type Checker: Polymorphic function `stream-append'
could not be applied to arguments:
Argument 1:
Expected: (Rec Stream (U (Boxof (U (-> (Pairof A Stream)) (Pairof
A Stream))) Null))
Given: (Rec x₀ (U (Boxof (U (-> (Pairof (Listof Number) x₀))
(Pairof (Listof Number) x₀))) Null))
Argument 2:
Expected: (Rec Stream (U (Boxof (U (-> (Pairof A Stream)) (Pairof
A Stream))) Null))
Given: (Rec x₀ (U (Boxof (U (-> (Pairof Number x₀)) (Pairof
Number x₀))) Null))

in: (stream-append (stream (drop-right xs 1)) (gfib_t xs))

Change (stream (drop-right xs 1)) to (apply stream (drop-right xs 1))
and you should be OK.

(It might be possible to call stream-append with a list and a stream
--- like the untyped code does --- but I haven't figured out how to do
that. Better stick with the Stream datatype.)

[Kiong-Gē Liāu]

Ben, 

Thanks, changing "stream" to "stream apply" does solve the issue. 

I tried to push it further little bit with the following code to see if typed racket can support generic like Haskell or Scala: 

#lang typed/racket

(require pfds/stream)

(define-type (OverFoldable A) (-> (Listof A) A))

(define-type (FibStreamCons A) (-> (Listof A) (Stream A)))

(define-type (FibStream A) (-> (OverFoldable A) (Listof A) (Stream A)))

(: sum (OverFoldable Number))

(define (sum xs) (apply + xs))

(: gfib_2 (All (A) (FibStream A)))

(define (gfib_2 f xs)

  (: gfib_t (All (A) (FibStreamCons A)))

  (define (gfib_t ys) 

    (stream-cons (last ys) (gfib_t (append (cdr ys) (list (f ys))))))

  (stream-append (apply stream (drop-right xs 1)) (gfib_t xs)))

However, I got the following error message:

; /home/kiong-ge/Programming/Racket/typed_racket_test.rkt:28:61: Type Checker: type mismatch

;   expected: (Listof A)

;   given: (Listof A)

;   in: ys

But, according to this error message, expected and given types are exactly the same, not sure how to deal with this issue. 

Thanks, 

Kiong-Gē. 

[Ben Greenman]

I think the problem is 2 different type variables that both print as
the letter A.

When I remove the "All" from the type for gfib_t (FibStreamCons A), it
typechecks.

[Kiong-Gē Liāu]

Thanks, following Ben's suggestion that follow code works 

#lang typed/racket

;; 

(require pfds/stream)

;; 

(define-type (OverFoldable A) (-> (Listof A) A))

;; 

(define-type (FibStreamCons A) (-> (Listof A) (Stream A)))

;; 

(define-type (FibStream A) (-> (OverFoldable A) (Listof A) (Stream A)))

;; 

(: sum (OverFoldable Number))

(define (sum xs) (apply + xs))

;; 

(: gfib (FibStream Number))

(define (gfib f xs)

  (: gfib_t (FibStreamCons Number))

  (define (gfib_t ys) 

    (stream-cons (last ys) (gfib_t (append (cdr ys) (list (f ys))))))

  (stream-append (apply stream (drop-right xs 1)) (gfib_t xs)))

;; 

(: gfib_2 (All (A) (FibStream A)))

(define (gfib_2 f xs)

  (: gfib_t (FibStreamCons A))

  (define (gfib_t ys) 

    (stream-cons (last ys) (gfib_t (append (cdr ys) (list (f ys))))))

  (stream-append (apply stream (drop-right xs 1)) (gfib_t xs)))

;; 

(define gfib2_0 

  (gfib sum '(0 1)))

;; 

(stream->list (take 30 gfib2_0))

;; 

(define gfib2_1 

  (gfib_2 sum '(0 1)))

;; 

(stream->list (take 30 gfib2_1))

;; 

(= (last (stream->list (take 201 gfib2_1)))

   (last (stream->list (take 201 gfib2_0))))

;; typed_racket_test.rkt ends here

[Ben Greenman]

On 7/14/21, Kiong-Gē Liāu <gongy...@gmail.com> wrote:
> Thanks, following Ben's suggestion that follow code works

Great!