Transform ML код F # (выше-kinded полиморфизм)

Question

Я пытаюсь следить на бумаге «Lightweight высших kinded полиморфизм» (https://ocamllabs.github.io/higher/lightweight-higher-kinded-polymorphism.pdf) и я застрял на преобразовании этого ML кода в F #

type (_,_) arrow = 
    Fn_plus : ((int ∗ int), int) arrow 
    | Fn_plus_cons : int → ((int ∗ int list), int list) arrow 

и

let apply : type a b. (a, b) arrow ∗ a → b = 
    fun (appl, v) → match appl with 
    | Fn_plus → let (x, y) = v in x + y 
    | Fn_plus_cons n → let (x, l’) = v in x + n :: l’ 

в частности, определение типа чувствует себя как большой волшебной стеной.

Answer 1

В этом примере используются GADT (вроде подобных дискриминируемых объединений, где отдельные случаи объединения могут ограничивать параметры типа по-разному), которые недоступны в F #. К счастью, это всего лишь часть введения в идею децентрализации (ценности), поэтому я думаю, что это не является критическим для той части бумаги, о которой вы заботитесь.

Как один из способов кодирования GADT на языке с более родственными типами показан here, поэтому вы можете фактически кодировать GADT, используя подход «Легкий более высокий сорт полиморфизма».

Другой, более простой подход показан в разделе «Упрощенный GADT» here, который в основном упрощен для перевода на F #. Однако обратите внимание на предостережение, упомянутое здесь, что принцип Лейбница не совсем полностью поддерживается (и посмотрите на другие разделы страницы, чтобы увидеть превосходное расширение подхода, которое снова требует более высоких видов).