Как определить экземпляр полиморфной структуры данных Union в Typed Racket?

Из Руководства по типизированному рэкету, чтобы определить тип объединения, просто используйте (define-type Some-Type (U Type1 Type2)) .

Чтобы определить полиморфные структуры данных, используйте что-то вроде (define-type (Opt a) (U ...)).

Я хочу определить полиморфное бинарное дерево

(define-type (Tree a) (U (Leaf a) Node))
(struct (a) Leaf ([val : a]))
(struct Node ([left : Tree] [right : Tree]))
(define t1 (Leaf 5))
(define t2 (Leaf 8))
(define t3 (Node t1 t2))

Мне было интересно, почему тип t1 — Leaf, а не Tree, и как сделать так, чтобы он был Tree?

> t1
- : (Leaf Positive-Byte)
#<Leaf>

racket typed-racket
person hellotli    schedule 16.01.2016    source источник

Ответы (2)


arrow_upward
4
arrow_downward

Когда вы делаете это:

(define-type (Tree a) (U (Leaf a) Node))

Вы определяете Tree как конструктор типа. Вы не должны думать о самом Tree как о типе, только о (Tree Some-Concrete-Type) как о типе. Поэтому переименуйте его в Treeof:

(define-type (Treeof a) (U (Leaf a) Node))
(struct (a) Leaf ([val : a]))
(struct Node ([left : Treeof] [right : Treeof]))

Теперь проблема яснее. Структура узла ожидает Treeof, но дерево чего? Что вы хотите, так это:

(define-type (Treeof a) (U (Leaf a) (Node a)))
(struct (a) Leaf ([val : a]))
(struct (a) Node ([left : (Treeof a)] [right : (Treeof a)]))

Теперь ваш пример работает:

#lang typed/racket
(define-type (Treeof a) (U (Leaf a) (Node a)))
(struct (a) Leaf ([val : a]))
(struct (a) Node ([left : (Treeof a)] [right : (Treeof a)]))
(define t1 (Leaf 5))
(define t2 (Leaf 8))
(define t3 (Node t1 t2))
person Alex Knauth    schedule 16.01.2016
comment
Когда я определяю что-то вроде (define t3 (Node (Leaf 3) (Node (Leaf 5) (Leaf 8)))) , возникает ошибка типа. - person hellotli; 17.01.2016
comment
Хм. Это подходит для меня. Какую версию ракетки вы используете? В любом случае вы можете исправить это, добавив явную аннотацию типа или используя inst. (: t3 : (Treeof Integer)) (define t3 (Node (Leaf 3) (Node (Leaf 5) (Leaf 8)))) вам подходит? - person Alex Knauth; 17.01.2016

arrow_upward
1
arrow_downward

См. ссылку о подтипах (https://docs.racket-lang.org/ts-guide/types.html#%28part._.Subtyping%29). По сути, когда вы используете тип union, Racket не уничтожает старые типы. Например, вы можете определить тип (U String Number), но String и Number по-прежнему можно будет использовать. 1 по-прежнему будет распознаваться как Number, но вы можете использовать его в любых местах, где ожидается (U String Number), потому что Number является подтипом (U String Number).

Точно так же t1 является Leaf, поэтому нет ничего плохого в том, что Racket сообщает, что t1 является Leaf. Однако Leaf является подтипом Tree, поэтому t1 можно использовать там, где ожидается Tree.

person Sorawee Porncharoenwase    schedule 16.01.2016