насладился тем фактом, что надо делать 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 по дефолту нужна?
у пурсы так, eta-expansion надо делать почти всегда
Обсуждают сегодня