Dependent types in half of D

Посмотрел тут свежее выступление одного из активных пильщиков Идриса: David Christiansen - Coding for Types: The Universe Patern in Idris. Он там рассказывает, что вот в языках с зависимыми типами у нас типы вроде как первоклассные, можно их как обычные значения создавать, передавать и использовать, но вот паттерн-матчить по ним не положено - это отнимет бесплатные теоремы (id может начать возвращать 42 для всех натуральных аргументов, например) и помешает стиранию этих типов из рантайма. Не положено (надо бы сказать "нельзя", но по крайней мере несколько версий назад кое-какой простой матчинг по типам там работал), но порой очень хочется. Для этого есть дизайн паттерн: The Universe Pattern, заключающийся в том, что для интересующего нас набора типов мы делаем тип данных, их кодирующий (аки AST), где хотим матчимся по нему, а когда нужны сами типы, то просто отображаем их из этой кодировки. Например, есть у нас таблички, где поля могут быть строками, целыми или вещественными числами. Описываем это алгебраиком:

data Column = TEXT | REAL | INTEGER

и сразу делаем отображение в "настоящие" типы:

interpCol : Column -> Type
interpCol TEXT -> String
interpCol REAL -> Double
interpCol INTEGER -> Integer 

Надо превратить поле одного из этих типов в строку? Пожалуйста:

printCol : (c : Column) -> interpCol c -> String
printCol TEXT    x = x
printCol REAL    x = doubleToString x
printCol INTEGER x = intToString x  

Тут функция с двумя аргументами, где тип второго зависит от значения первого, т.е. зависимые типы как они есть. Можно вызвать printCol TEXT "hi", а можно printCol INTEGER 77, но printCol TEXT 77 уже не скомпилируется, будет ошибка типов.
( Read more... )