Фрустрация.
Один из моих первых подходов к хаскелю оказался неудачным.
Я подумал, что я могу написать распознавание грамматик (не разбор, а всего лишь распознавание) следующим образом:
readNum n c = if isDigit c then (True, readNum (n++[c])) else (False,n)
skipSpace c = if isSpace c then (True,isSpace c) else (False,())
...
И потом придумать комбинатор, что вытаскивает по одному символу из потока, перебирает все альтернативы и отсекает те, где пришёл False.
То есть, понять, что такое ФВП я успел, но до алгебраических типов я не дошёл.
Само собой, я получал ошибки типов, сидел и недоумевал, как же так. Ведь ясно же, что вот, смотрите, если True, то одно, а если False, то другое! Вот, я на тикле так написал, всё работает!
Собственно, плюс динамической проверки типов в том, что она позволяет делать вот такие, кажущиеся логичными, варианты. И всё работает. Это такой "пофиморфизм" - пофигистичный полиморфизм.
Спустя 10 лет, в 2008 году я прочитал книгу Programming in Martin-Löf type theory, где списки вводятся похожим образом:
- есть перечислимые типы, один из них Bool: True:Bool, False:Bool, сам Bool принадлежит вселенной типов Bool:Set,
- есть зависимые пары, где тип второго аргумента зависит от первого: Π: a:Set:, B:Set: (A,A->B),
- есть функции из значений в типы.
Для описания моей первой попытки, мне бы пришлось написать тип вида:
recognitionFunction : {A : Set} -> Char -> ( x : Bool, recognitionContinuationType {A} x)
recognitionContinuationType : {A : Set} -> Bool -> Set
-- если True, то продолжаем:
recognitionContinuationType {A} True = recognitionFunction {A}
recognitionContinuationType {A} False = A
(набросок, поскольку давно уж не занимался Агдой)
Выводу типов это не подлежит, к сожалению. То есть, придётся писать дополнительные строки кода. А далее, как обычно: записав инвариант, мы получаем его проверку везде, где он упоминается.
Я подумал, что я могу написать распознавание грамматик (не разбор, а всего лишь распознавание) следующим образом:
readNum n c = if isDigit c then (True, readNum (n++[c])) else (False,n)
skipSpace c = if isSpace c then (True,isSpace c) else (False,())
...
И потом придумать комбинатор, что вытаскивает по одному символу из потока, перебирает все альтернативы и отсекает те, где пришёл False.
То есть, понять, что такое ФВП я успел, но до алгебраических типов я не дошёл.
Само собой, я получал ошибки типов, сидел и недоумевал, как же так. Ведь ясно же, что вот, смотрите, если True, то одно, а если False, то другое! Вот, я на тикле так написал, всё работает!
Собственно, плюс динамической проверки типов в том, что она позволяет делать вот такие, кажущиеся логичными, варианты. И всё работает. Это такой "пофиморфизм" - пофигистичный полиморфизм.
Спустя 10 лет, в 2008 году я прочитал книгу Programming in Martin-Löf type theory, где списки вводятся похожим образом:
- есть перечислимые типы, один из них Bool: True:Bool, False:Bool, сам Bool принадлежит вселенной типов Bool:Set,
- есть зависимые пары, где тип второго аргумента зависит от первого: Π: a:Set:, B:Set: (A,A->B),
- есть функции из значений в типы.
Для описания моей первой попытки, мне бы пришлось написать тип вида:
recognitionFunction : {A : Set} -> Char -> ( x : Bool, recognitionContinuationType {A} x)
recognitionContinuationType : {A : Set} -> Bool -> Set
-- если True, то продолжаем:
recognitionContinuationType {A} True = recognitionFunction {A}
recognitionContinuationType {A} False = A
(набросок, поскольку давно уж не занимался Агдой)
Выводу типов это не подлежит, к сожалению. То есть, придётся писать дополнительные строки кода. А далее, как обычно: записав инвариант, мы получаем его проверку везде, где он упоминается.