А еще я пописал на строгой System F omega и

Question

А еще я пописал на строгой System F omega и

насладился тем фактом, что надо делать eta-expansion вручную, иначе можно запросто влететь в бесконечный цикл. Например вот этот терм:

/\(r :: *) -> \(f : r -> r) ->
fix {r} {nat -> r} \(rec : r -> nat -> r) (z : r) (n : nat) ->
unwrap n {r} z (\(n' : nat) -> rec (f z) n')

вычисляется нормально. А вот этот зацикливается, насколько я помню:

/\(r :: *) -> \(f : r -> r) ->
fix {r} {nat -> r} \(rec : r -> nat -> r) (z : r) (n : nat) ->
unwrap n {r} z (rec (f z))

короче я люблю лень, просто нахрена она в data по дефолту нужна?

#haskell #programming #russian

0

25.05.2020

1 ответов

14 просмотров

Zygohistomorphic Prepromorphism🇺🇦 · Accepted Answer

Zygohistomorphic Prepromorphism🇺🇦

у пурсы так, eta-expansion надо делать почти всегда

0

25.05.2020

169 похожих чатов

А еще я пописал на строгой System F omega и

1 ответов

Похожие вопросы