LINUX.ORG.RU

История изменений

Исправление AndreyKl, (текущая версия) :

А как выглядит вызов?

К слову, на идрисе как то так. Правда я сменил условие выбора типа на булевское, но это не так важно. И не уверен что даже так скомпиляется (из за того что булевское и x /= 42 никак не связано). И пример, конечно, вырожденный: мы в итоге таскаем с собой булевское значение которое используем чтобы вывести на экран результат.

Но это именно из-за простоты примера. Вот тут у Брэди на ~ 10:50 показан типобезопасный printf с использованием этой техники. Т.е. это действительно рабочий инструмент.

module Main

toMaybeInt : String -> Maybe Int
toMaybeInt = ?toint

getType : (isInt : Bool) -> Type
getType False = String
getType True = Int

workingFunction : (x: Int) -> getType (x /= 42)
workingFunction 42 = "Мужик, это был смысл жизни, вселенной и всего такого!"
workingFunction x = x*2

showAnswer : (isInt : Bool) -> getType isInt -> String
showAnswer True i = "Квадрат числа равен" ++ show i
showAnswer False s = s

main : IO ()
main = do mbint <- map toMaybeInt getLine
          case map (\x => (x, x /= 42)) mbint of
            Just (x, isInt) => putStr $ 
                showAnswer isInt (workingFunction x)
            Nothing => putStr "Нужно вводить целое число"

Исходная версия AndreyKl, :

А как выглядит вызов?

К слову, на идрисе как то так. Правда я сменил условие выбора типа на булевское, но это не так важно. И не уверен что даже так скомпиляется (из за того что булевское и 42 == x никак не связано). И пример, конечно, вырожденный: мы в итоге таскаем с собой булевское значение которое используем чтобы вывести на экран результат.

Но это именно из-за простоты примера. Вот тут у Брэди на ~ 10:50 показан типобезопасный printf с использованием этой техники. Т.е. это действительно рабочий инструмент.

module Main

toMaybeInt : String -> Maybe Int
toMaybeInt = ?toint

getType : (isInt : Bool) -> Type
getType False = String
getType True = Int

workingFunction : (x: Int) -> getType (x == 42)
workingFunction 42 = "Мужик, это был смысл жизни, вселенной и всего такого!"
workingFunction x = x*2

showAnswer : (isInt : Bool) -> getType isInt -> String
showAnswer True i = "Квадрат числа равен" ++ show i
showAnswer False s = s

main : IO ()
main = do mbint <- map toMaybeInt getLine
          case map (\x => (x, x == 42)) mbint of
            Just (x, isInt) => putStr $ 
                showAnswer isInt (workingFunction x)
            Nothing => putStr "Нужно вводить целое число"