expanding to typed/racket using #lang turnstile

[Raoul Schorer]

Hi,

I am attempting to expand to typed/racket from a custom language through #lang turnstile. Unfortunately, the macro stepper isn't helping me much as to how I should do that.

So far, this minimal example:

#lang turnstile

(require (only-in (prefix-in tr: typed/racket)
                  tr:#%module-begin
                  tr:Number
                  tr:#%datum)
         turnstile/no-unicode)
(provide #%datum #%module-begin)

;[MODULE-BEGIN]
(define-syntax (#%module-begin stx)
  (syntax-parse stx
    [(_ prg) #`(tr:#%module-begin prg)]))

;[DATUM]
(define-typed-syntax #%datum
  [(_ . n:number) >>
   -------------------
   [/- (tr:#%datum . n) => tr:Number]])

returns an error when I try to type a number in the REPL:

> 1
  type-check: type name used out of context
  type: tr:Number
  in: tr:Number in: tr:Number

I am a bit lost. Could someone give me pointers on how to expand to typed/racket types using turnstile, please?

Thanks a lot!

Raoul

[William J. Bowman]

This might be too minimal of an example.
It looks like typed Racket doesn't want you to use Typed Racket types in certain
contexts.
To implement the functionality I think you want from that example, I would
write the following

#lang turnstile

(require (only-in (prefix-in tr: typed/racket)

tr::print-type
tr:ann

tr:#%module-begin
tr:Number
tr:#%datum)
turnstile/no-unicode)

(provide #%datum (rename-out (tr:#%module-begin #%module-begin)))

;[DATUM]
(define-typed-syntax #%datum
[(_ . n:number) >>
-------------------

[≻ (tr:ann (tr:#%datum . n) tr:Number)]])


You probably need to use a Turnstile types in your language, and generate Typed
Racket types using the `ann` form from Typed Racket.

--
William J. Bowman

> --
> 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/b9b56563-3a18-406d-9f2f-935220673b79%40googlegroups.com.

[Stephen Chang]

As William mentioned, the example conflates Typed Racket types with
surface language types, which would probably not be right even if
Typed Racket did not complain.

Does your custom language have its own type system? If not, you may
not need to use Turnstile. Plain macros that expand to Typed Racket
might suffice.

To better help you, would you be willing to describe some more details
about your custom language?

> To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/20191029173336.GJ2191%40williamjbowman.com.

[Raoul Schorer]

Thank you very much for taking the time to help me.

I am trying to write an extendable APL with full type inference and optional type annotation. Essentially, I am trying to compile J. J cannot be compiled efficiently because the ambiguities of its grammar lead to combinatory explosion of conditional branches in the resulting AST. The optional type annotations would therefore allow to prune the AST.

You can find an example of this problem here:

https://www.reddit.com/r/apljk/comments/bw8s49/question_regarding_the_impossibility_of_compiling/epwfgfq/

In practice, instead of writing

g =: + f (1 2 3 4 5)

where f has an ambiguous type (Union (-> (Array Number) (Array Number)) (-> (-> Array Number) (-> Array Number))), I would write something like

g =: + 3::f (1 2 3 4 5)

Where 3:: represents a type annotation meaning (-> (Array Number) (Array Number))

Type inference in the language can however be derived directly from the execution model represented by the parse table at https://www.jsoftware.com/help/jforc/parsing_and_execution_ii.htm instead of a traditional inference algorithm. You can find my stub attempt with syntax/parse only at https://github.com/Rscho314/jacket/blob/master/parser.rkt

Perhaps I should persevere with syntax/parse only? Or maybe it would be better to use type.expanders in the codegen phase instead of trying to do all at once with turnstile?

I hope I am being clear. I'm just a hobbyist and have no formal CS education.

Thanks again!

[Stephen Chang]

I dont know much about J, but if I'm understanding correctly, you have
an implementation of J in Typed Racket?

And then you want to be able to infer more specialized cases in some
instances by pruning the type?

You might be able to do it with just plain macros in that case, which
would generate `ann` like William suggested to simplify some types.

Here's an example that does something similar for things like regexp:
https://blog.racket-lang.org/2017/04/type-tailoring.html

> --
> 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/99b623eb-fbd9-4dfa-b510-7451e4ef2dac%40googlegroups.com.