Типы разностных объединений и различающиеся объединения машинописный текст / F #

Question

Итак, я читал официальную документацию Typescript о типах объединения и думал, что это то же самое, что и «размеченные объединения» в F # (при условии, что у них другой синтаксис, но та же концепция), поскольку у меня есть фон F # и учитывая тот факт, что оба они поддерживаются Microsoft. Но, глядя на документацию, F # на самом деле не делает различий между «типами объединения» и «размеченными союзами»: https://fsharpforfunandprofit.com/posts/discriminated-unions/

Однако Typescript делает различие между этими двумя концепции:

Типы объединения: https://www.typescriptlang.org/docs/handbook/advanced-types.html#union -типы

Дискриминируемые союзы: https://www.typescriptlang.org/docs/handbook/advanced-types.html#discriminated -союзные

Итак, я было интересно, действительно ли существует различие в самих концепциях или это просто понятие, зависящее от языка?

На данный момент я понимаю, что типы объединения в F # также являются дискриминируемыми объединениями, потому что вы можете различать тип объединения, используя выражения соответствия и деконструкцию. язык не предоставляет для этого специального c выражения, поэтому вам нужно различать дискриминант по значению, которое есть у всех типов объединения. Это правильно?

Answer 1

Основное отличие состоит в том, что Typescript Union Type на самом деле является надмножеством F # Discriminated Union.

TypeScript Union Type = Untagged тип объединения.
F # Discriminated Union = Tagged union type.

Другими словами, каждое дискриминированное объединение которые можно смоделировать в F #, можно смоделировать изоморфно в типе объединения Typescript, однако обратное неверно.

Например, следующее размеченное объединение в F #:

type a' Option = Some of 'a | None 

Можно смоделировать изоморфно в Typescript как:

type Option<T> = {tag: 'Some', value: T} | {tag: 'None'}

Однако следующий тип объединения Typescript не может быть смоделирован изоморфно в F #:

type UserInput = number | string

Основное различие здесь - тип объединения TypeScript не должен быть помечен , однако тип объединения F # должен быть помечен.

Таким образом, мы видим, что TypeScript на самом деле более гибкий, чем F #, однако это не обходится без затрат, без тегов union на самом деле дырявые, что означает, что есть какое-то объединение типов, где TypeScript не сможет выполнить проверку типа.

Это похоже на то, что нетиповое лямбда-исчисление является надмножеством типизированного лямбда-исчисления, но типизированное лямбда-исчисление намного легче доказать правильно.

Answer 2

Операнды в объединении типов (A | B) являются обоими типами, тогда как регистры в размеченном объединении type U = A | B являются конструкторами для типа U и не являются типами сами по себе. Значения типа U помечаются во время выполнения, поэтому вы можете различать guish между возможными случаями.

Одним из следствий этого является то, что размеченные объединения могут быть вложены так, как типы объединения не могут. Необязательные значения некоторого типа A в системе типов объединения могут быть представлены как

type A? = (A | null)

, где null - одноэлементный тип для значения null.

С дискриминированным union это обычно представляется как

type a' option = Some of 'a | None 

В этой формулировке значение

let o: int option option = Some None

не может быть представлено с типом union, поскольку (A?)? == (A | null) | null == A | null == A?