Control.ST чистый тип - PullRequest
Новая
       42

Control.ST чистый тип

0 голосов
/ 01 декабря 2018

pure : (result : ty) -> STrans m ty (out_fn result) out_fn из http://docs.idris -lang.org / ru / latest / st / state.html # strans-primitive-operations

Я не уверен, что (out_fn result) out_fn средства.Об ограничении out_fn функцией result?Означает ли это что-нибудь о списке входных ресурсов?

Данное объяснение выглядит как "... при условии, что текущий список ресурсов корректен при создании этого значения" , но я 'я не уверен, как это интерпретировать.

1 Ответ

0 голосов
/ 02 декабря 2018 
STrans : (m : Type -> Type) ->
         (result : Type) ->
         (inRes : Resources) ->
         (outRes : result -> Resources) ->
         Type

Вы видите, что входные ресурсы не зависят от результата вычисления, но выходные ресурсы делают.Теперь, скажем, у нас есть 

MyResultType : Type
myResult : MyResultType

Какого типа pure myResult?Это STrans m MyResultType (f myResult) f.Каковы входные ресурсы?f myResult, который может быть чем угодно.Каковы выходные ресурсы?Ну, это зависит от результата.Но это pure, поэтому результат всегда myResult, поэтому выходные ресурсы также равны f myResult.Вы видите, что подпись pure говорит о том, что ресурсы ввода и вывода могут быть чем угодно, и что «что угодно» зависит от f и myResult, но они должны быть одинаковыми «что угодно», несмотря ни на что.

Я считаю, что эквивалентный способ увидеть тип pure - это 

pure' : (result : ty) -> STrans m ty resources (const resources)

Что, вероятно, более понятно.Я не знаю, почему эта подпись не используется.

...