polymorphic datastructures in typed/racket

[bedeke]

Hello,

I was trying to type some polymorphic classes but I got stuck early on making a polymorphic subclass

#lang typed/racket/base

;*****1*****
(require typed/racket/class)

(define-type (C-class A)(Class [init-field [x A]]))

(define C1%
 (class object%
 #:∀ (A)
 (init-field [x : A])
 (super-new)))

(define C2%
 (class (inst C1% A)
 #:∀ (A)
 (super-new)))

(new (inst C2% Integer) [x 4])

C1% is recognised as a C-class, but explicitly calling C1% a C-class (omitting the #:forall (A) ) doesn't work

In the next step I don't seem to find the right way to make C2% a polymorphic subclass of C1%

Having failed that I went with structures. This I got mostly working, but I would like to have some niceties.

One was to parameterize a structure, but this lead to a problem of not being able to check some

types at runtime. I thought I got close, but I stranded on getting fields of structures without knowing the instantiation type

;*****2*****
(struct (A) S ([f1 : (-> A A A)]
               [f2 : (-> A Boolean : A)]))

(: S-of-type? (-> (-> Any Boolean : A) Any Boolean
                  : #:+ (implies #t (S A))
                    #:- (implies #f (! (S A)))))
(define (S-of-type? fct A)
  (and (S? A) (eq? fct (S-f2 A))))
;                      ^ how can I acces a field of this polymorfic struct

And another thing I tried but failed to get working is to sub-type a structure based

on a narrower type for one of the fields.

;*****3*****
(struct (A) B ([f1 : (Vectorof A)]
               [f2 : Integer])
  #:transparent)

(: B1? (All (A) (-> (B A) Boolean)))
(define (B1? b)(= (B-f2 b) 1))
(define b (B (vector 3) 1))
(assert b B1?)
b
(define-type B1 B1?)
;(define-new-subtype B1 B1?)
;(define-type B1 (All (A)(Struct (B (Vectorof A) 1))))

Are any of these things doable? Or are there better ways to tackle this problems?

What I got working is in

https://github.com/bdeket/polynomials/blob/alg-dic-pol/polynomials/math/private/polynomial/poly-struct.rkt (WIP)

Kind regards,

Bert

[bedeke]

Hi,

I managed to do the second part using prefab structures, but then I can't be sure it was created with the right constructor.

Since it seems not doable to get this working with classes I will go back to untyped code.

[Sam Tobin-Hochstadt]

A few thoughts on this:

First, polymorphic data structures are certainly supported in Typed
Racket. You might be interested in https://github.com/takikawa/tr-pfds
which is a library of them.

Second, it's not totally clear to me what you're trying to do in your
various code snippets. Here's a working version of your first code
snippet, but since I don't know what you're trying to do I'm not sure
if it works with the larger goals you have:

```

#lang typed/racket/base

;*****1*****
(require typed/racket/class)

(define-type (C-class A)
(Class [init-field [x A]]))

(define C1%
(class object%
#:∀ (A)
(init-field [x : A])
(super-new)))

(: C2% (All (A) (-> (C-class A))))
(define (C2%)
(class (inst C1% A)
(super-new)))

(new ((inst C2% Integer)) [x 4])
```

Third, your version with structs can't work because you can't tell
what type a function expects -- that information is not there at
runtime.

Sam

> --
> 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/3c4bcedd-5677-4972-97a3-04e33ca30816%40googlegroups.com.

[David Storrs]

On Mon, Nov 18, 2019 at 10:09 AM Sam Tobin-Hochstadt <sa...@cs.indiana.edu> wrote:

Third, your version with structs can't work because you can't tell
what type a function expects -- that information is not there at
runtime.

If there is a contract assigned to a function, is it possible to get that function and analyze it?

To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/CAK%3DHD%2BaE1h7tYT4nyRoAgUhVCWCNmJfvJ5V5QTzCcbwv_kvJhA%40mail.gmail.com.

[David Storrs]

On Mon, Nov 18, 2019 at 12:23 PM David Storrs <david....@gmail.com> wrote:

On Mon, Nov 18, 2019 at 10:09 AM Sam Tobin-Hochstadt <sa...@cs.indiana.edu> wrote:

Third, your version with structs can't work because you can't tell
what type a function expects -- that information is not there at
runtime.

If there is a contract assigned to a function, is it possible to get that function and analyze it?

Correction:  Get that *contract* and analyze it.

[Sam Tobin-Hochstadt]

It is possible to get the contracts of values, (see `value-contract`)
but Typed Racket doesn't know how to do that, and it would be
problematic anyway since the value isn't around until runtime, but TR
runs at compile time.

Sam

> To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/CAE8gKodq4Y_sFnCdTXtOP4OrZxckhajxejOOqwyN3j0wTe7_EQ%40mail.gmail.com.

[bedeke]

Classes:

cool, so I can make a function that produces a polymorphic subclass of C1, but not a straight polymorphic subclass. I can work with that.

It seems in this case, if I want to implement a new method for the subclass C2 I can not use

```

(define-type (D-class A)(Class ... #:implements (C-class A) ...)

```

Or is there also a special way to make this work?

If not, at least I can define a new type in which I copy the complete Class type again + the new method, so it's not a big problem.

Structs:

what I got working was this:

```

#lang typed/racket/base

(struct (A) S ([f1 : (-> A A A)]

               [f2 : (-> Any Boolean : #:+ A)])
  #:prefab
  )

(: S-of-type? (All (A) (-> Any
                           (-> Any Boolean : #:+ A)
                           Boolean
                           : #:+ (implies #t (S A)))))
(define (S-of-type? obj fct) (and (S? obj)(eq? fct (S-f2 obj))))

(define C ((inst S Number) + number?))
(S-of-type? C number?)
(S-of-type? C real?)

```

It works on a prefab structure, but not on a normal structure. I was hoping to use this as a way to get the type at runtime. But since it only works with prefab structures, It doesn't work... (or better said, too many objects can pass this test).

For a normal structure I hoped the guarantee that it was created with (S ...) would be enough extra info to be sure that if f2 is eq? then S must be of type A for f2 of type (-> Any Boolean : #:+ A)

But anyway, I feel that for what I need, classes are really the better option, so I will try to type it with the tip you gave me, or if that doesn't work, go for untyped.

Thank you very much,

Bert

On Monday, 18 November 2019 20:30:09 UTC+1, Sam Tobin-Hochstadt wrote:

It is possible to get the contracts of values, (see `value-contract`)
but Typed Racket doesn't know how to do that, and it would be
problematic anyway since the value isn't around until runtime, but TR
runs at compile time.

Sam

On Mon, Nov 18, 2019 at 12:24 PM David Storrs <david...@gmail.com> wrote:

>>> > To unsubscribe from this group and stop receiving emails from it, send an email to racket...@googlegroups.com.

>>> > To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/3c4bcedd-5677-4972-97a3-04e33ca30816%40googlegroups.com.
>>>
>>> --
>>> 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...@googlegroups.com.

>>> To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/CAK%3DHD%2BaE1h7tYT4nyRoAgUhVCWCNmJfvJ5V5QTzCcbwv_kvJhA%40mail.gmail.com.
>
> --
> 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...@googlegroups.com.