Что можно почитать о способах по перегонке инвариантов из гардов

Question

Haskell

Alex

Что можно почитать о способах по перегонке инвариантов из гардов

в типы?

#haskell #programming #russian

0

30.06.2022

9 ответов

19 просмотров

IC Rainbow

GADTs?

0

30.06.2022

Kirill Valyavin

Самый простой вариант: data PossiblyInvalid data Valid data WhatWentWrong parse :: PossiblyInvalid -> Either WhatWentWrong Valid lookMaNoGuards :: Valid -> IO ()

0

30.06.2022

Cheese Syrowiecki

если речь о типе, представляющем число в фиксированном диапазоне, то это вроде называется refinement types, и есть 2 основных подхода к ним: 1) обернуть обычное число в newtype и валидировать его на входе. 2) придумать такое представление, любое значение в котором взаимно однозначно соответствует объекту из домена

0

30.06.2022

Alex Автор вопроса

Cheese Syrowiecki
если речь о типе, представляющем число в фиксирова...

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

0

30.06.2022

Kirill Valyavin

Alex
а если много вычислений внутри алгоритма. т.е. дан...

Можно с помощью тайпчекера подоказывать, что преобразования не ломают инварианты, для этого есть завтипы (в Haskell поддерживается частично с помощью расширений), рефайнменты в реализации Liquid Haskell, и подход/библиотека ghosts of departed proofs Но это всё довольно муторно

0

30.06.2022

Kirill Valyavin

Alex
а если много вычислений внутри алгоритма. т.е. дан...

Если возможно выделить набор заведомо сохраняющих инварианты операций, можно из них составить eDSL, и тогда любая программа на нём будет корректной без лишних проверок

0

30.06.2022

Alex Автор вопроса

Kirill Valyavin
Если возможно выделить набор заведомо сохраняющих ...

а есть какой-то инженерно-прагматичный материал по теме?

0

30.06.2022

Kirill Valyavin

Alex
а есть какой-то инженерно-прагматичный материал по...

Насчёт материалов не уверен, но могу попытаться ответить на вопросы, если они есть

0

30.06.2022