Polymorphic datatype

[markfarrell]

Allows define-datatype to take type parameters, as discussed in https://github.com/andmkent/datatype/issues/2.

e.g.

(define-datatype (Optional a)
  [Some (a)]
  [None ()])

Note: changes syntax of define-datatype; might not be quite ready to merge for that reason, if e.g. examples need to be updated.

cc/ @andmkent

[pnwamk]

Cool - let me look at adding a few tweaks so specifying type variables is optional (i.e. the old syntax is valid too) and I'll report (today or tomorrow).

[markfarrell]

Yeah, sounds good. :+1:

[markfarrell]

Easiest solution involves duplicate code. Should be possible to simplify?

[markfarrell]

On a related note: having an issue with a "polymorphic" type-case and likewise match:

(: a (Optional String))
(define a
  (Some "test"))

(: b String)
(define b 
  (type-case Optional a
    [(Some str) => str]
    [else => "error"]))

(: c String)
(define c
  (match a 
    [(Some str) str]
    [_ "error"]))

. Type Checker: type mismatch
  expected: String
  given: Any in: str
. Type Checker: type mismatch
  expected: String
  given: Any in: str
. Type Checker: Summary: 2 errors encountered in:
  str
  str

Currently have to cast to resolve:

(: a (Optional String))
(define a
  (Some "test"))

(: b String)
(define b 
  (type-case Optional a
    [(Some str) => 
     (cast str String)]
    [else => "error"]))

(: c String)
(define c
  (match a 
    [(Some str) 
     (cast str String)]
    [_ "error"]))

[pnwamk]

Duplicate code: We should be able to use the features of the syntax/parse library to avoid duplicate code (using features like ~or, ~bind, and syntax classes).

Polymorphic issues: There's a fundamental issue with the current approach: assigning polymorphic variables to a struct that does not have any fields of the polymorphic type in essence ignores the polymorphic variables. For example, the following typechecks:

#lang typed/racket

(struct: (A) Foo () #:transparent)

(define (foo [x : (Foo Integer)]) : (Foo String)
  x)

I think this indicates I need to rewrite things to use a define-type and a union instead of an empty parent struct and inheritance.

[pnwamk]

Yikes - tinkered with that a little longer than I thought I would =)

Well for now I threw together something that supports both non-polymorphic and polymorphic definitions:

#lang typed/racket

(require "datatype.rkt")
(define-type Int Integer)

(define-datatype (Opt A)
  [Some (A)]
  [None ()])

(define (extract-int [x : (Opt Int)]) : Integer
  (Opt-case [#:inst Int]
   x
   [(Some i) => i]
   [(None) => -1]))

(define-datatype Expr
  [Var (Symbol)]
  [Lambda (Symbol Expr)]
  [App (Expr Expr)])

(: foo (Expr -> Symbol))
(define (foo e)
  (Expr-case
   e
   [(Var x) => x]
   [(Lambda y _) => y]
   [(App _ _) => 'app]))

I ended up just rewriting it from scratch more or less---I think it's a little easier to read now, with the catch being it no longer does the crazy macro generating macro stuff and now there is not a universal type-case but a case macro generated for each datatype. I'm sure with a little effort you could merge something like what I threw together here with the type-case stuff in the original definitions.

I don't have a lot of time to dedicate to this right now so... I'll leave what I have so far and if you like you can tweak/modify/etc... it however you see fit.

[pnwamk]

Oh - and the syntax choices were rather arbitrary (e.g. [#:inst ...] was easy to parse =)-- so if you wanted to play around with it and pick something that looks better or is easier to read/type etc... by all means! =)

[markfarrell]

Cool - thanks!