That's currently what I'm doing. The `list->array' function receives a
predicate that identifies the elements' type.
There are cases where no predicate exists, though (functions, most
obviously), so I needed another solution. Special array-constructing
syntax is turning out to be a nice one. I'm working on it now.
Interestingly, I still need to distinguish between (syntax) lists that
are meant to be rows and (syntax) lists that are meant to be elements.
I'm detecting bracket shape for that. So this is an array of vectors:
> (array [(vector 1 2) (vector 3 4)])
- : (View-Array (Vector Integer Integer))
(view-array ['#(1 2) '#(1 2)])
This is an array of something else:
> (array [vector 1 2])
- : (View-Array (U Positive-Byte (All (a) (a * -> (Vectorof a)))))
(view-array [#<procedure:vector> 1 2])
And this is an error:
> (array (1 2))
Type Checker: Cannot apply expression of type One, since it is not a
function type in: (1 2)
As a bonus, I'll finally be able to make printed arrays read as
equivalent arrays, if their elements are readable.
Neil ⊥
On 08/07/2012 12:11 PM, Sam Tobin-Hochstadt wrote:
Yes, if you can do that, then it will all work nicely.
On Tue, Aug 7, 2012 at 1:59 PM, Robby Findler
<[email protected]> wrote:
Altho in Neil's case, it maybe that he can positively state the types
allowed in the leaves.
Robby
On Tue, Aug 7, 2012 at 12:55 PM, Sam Tobin-Hochstadt <[email protected]> wrote:
More generally, this is a case where you want some form of negation
(plus bounded polymorphism) in the type system, but that's not
something I know how to add straightforwardly to Typed Racket.
Sam
On Tue, Aug 7, 2012 at 1:07 PM, Eric Dobson <[email protected]> wrote:
No it is not possible to type flatten.
Consider having flatten with this type:
(define-type (Listof* A) (Rec T (U A (Listof T))))
(: flatten (All (A) ((Listof* A) -> (Listof A))))
And then applying it as such:
((inst flatten (Listof Number)) (list (list 1 2 3)))
This would typecheck and return the value (list 1 2 3) with the type
(Listof (Listof Number)).
This is bad and breaks soundness.
On Tue, Aug 7, 2012 at 9:57 AM, Neil Toronto <[email protected]> wrote:
Short version: Creating arrays from nested lists (and vectors) would be a
lot easier if I could write a `flatten' function in TR, but I haven't been
able to. Is it possible?
Long version: Given this type:
(define-type (Listof* A) (Rec T (U A (Listof T))))
I'd like this function:
(: flatten (All (A) ((Listof* A) -> (Listof A))))
When I use `require/typed' to get it, it won't work:
(flatten 0)
- : (Listof Zero)
'(0)
(flatten '(0 1))
flatten: contract violation
two of the clauses in the or/c might both match: ...
The problem is that an `A' might be a (Listof B), so the generated contract
is ambiguous. The ambiguity also shows up in TR, though it's harder to
understand from the error message:
(: flatten (All (A) ((Listof* A) -> (Listof A))))
(define (flatten lst)
(cond [(list? lst) (append* ((inst map (Listof A) (Listof* A))
flatten
lst))]
[else (list lst)]))
Expected (Listof (Rec T (U A (Listof T))))
but got (U (Listof (Rec T (U A (Listof T))))
(Pairof Any (Listof Any)))
I think this error message is saying that if `lst' is a list, it really
could be any kind of list. I can't argue with that.
Is there a way around this particular error message?
More generally, is it possible to write `flatten' at all?
Neil ⊥
_________________________
Racket Developers list:
http://lists.racket-lang.org/dev
_________________________
Racket Developers list:
http://lists.racket-lang.org/dev
--
sam th
[email protected]
_________________________
Racket Developers list:
http://lists.racket-lang.org/dev
_________________________
Racket Developers list:
http://lists.racket-lang.org/dev
