#о системах типов и вообще о том, почему иногда рано праздновать победу
Cколько же есть вещей, без которых можно жить
-- Сократ
Карл пятый Римский Император говаривал, что
Ишпанским языком с Богом, Францусским с друзьями,
Немецким с неприятельми, Италиянским с женским полом
говорить прилично
-- Михаил Ломоносов
Пролог
thesz провел тут на днях разведку боем в стане Лисперов, в ходе которой произошло в частности некоторое количество бессмысленных сражений "статическая типизация vs. динамическая".
Вот, что лично я думаю по этому поводу. Во-первых, человек который рассуждает о достоинствах и недостатков языков никогда не должен забывать, о том, что в подобных сравнениях всегда существует субъективная и объективная. Спорить о субъективных сторонах не имеет особого смысла. Тем более не имеет никакого смысла вскользь называть кого-то "тормозами прогресса" основываясь исключительно на субъективных предпочтениях. Если честно, я никогда особо не разделял этузиазма "лигвистических адептов", которые только что не далают себе татуировку с эмблемой любимого ЯП на лбу или чуть выше лобка.
Когда таких адептов просишь привести какие-то объективные доказательства того, что язык A превосходит язык B, то либо слышишь в ответ лишь субъективные доказательства, либо доказательства, которые тянут за собой целый хвост "если бы".
Лично мое мнение таково... Плодитесь и размножайтесь... ЯП создавались/создаются и будут создаваться с единственной целью --- облегчить общение человека с различными электронными штуковинами. В этом отношении статическая и динамическая типизация это всего-лишь две стороны одной медали. Если оратору-программисту удобно использовать определенный язык для того что бы сказать определённую фразу определенной штуковине, то пусть он его и используется, а всё остальное суета сует и томленье духа. Не очень оригинально? Согласен, зато неоспоримо. Не верите, попробуйте оспорить. Только перед тем как оспаривать задумайтесь, есть ли у вас объективные критерии не завязанные на "если бы"? Можно конечно предложить какое-нибудь состязание, например, написание какого-нибудь компилятора, но оно ровным счётом ничего не покажет и ничего никому не докажет =)
Пример с моей любимой монадой
Ну вот возмём, например, поставленную мной задачу о создании монады, которая заставила бы работать вот такой код:
test = do put 1
cc <- getCC
x <- get
if x /= 10 then do put (x + 1)
cc
else do return x
Я некоторое продлолжительное время над ней тупил*, пытаясь придумать подходящий тип, бросал и брался снова... Пока наконец не догадался, что тип тут подходящий имеет вид
data M s a = A (s -> Integer -> (Either Integer a, s))
| forall b . C (M s b) (b -> M s a)
Этот тип представляет собой своего рода систему комманд для высокоуровневую виртуальную машину, которая умеет выполнять атомарные и неатомарные цепные действия. Цепные действия не особо интересны, поскольку являются калькой с операции >>= для монад. Атомарные действия представляют собой изуродованную монаду State: они имеют побочные эффекты в том смысле что они получают на вход состояние и возвращают возможно измененное состояние в качестве одного из возвращаемых значений. Кроме всего прочего действия могут иметь и обычное возвращаемое значение, либо вернуть некоторый числовой маркер... В этих числовых маркерах и кроется грязный хак: они обозначают уровень вычислений, на который следует откатиться. Что бы понять смысл этих маркеров посмотрим на реализацию интерпретатора, который собственно реализует нашу виртуальную машину. Интерпретатор реализуется функцией eval, которая получает действие, которое следует выполнить, активный маркер и текущее состояние.
eval (A f) i s = let (r, s') = f s i in case r of
Left i' -> if i == i' then eval (A f) i s' else (Left i', s')
Right a -> (Right a, s')
Видно результат выполнения атомарного действия, может сказать интерпретатору: вычисли меня еще раз. Это происходить если маркер текущего уровня совпадает, с маркером уровня на который мы хотим откатиться.
eval (C f g) i s = let (r, s') = eval f (i + 1) s in case r of
Left i' -> if i == i' then eval (C f g) i s' else (Left i', s')
Right b -> let v = g b
(r', s'') = eval v (i + 2) s' in case r' of
Left i' -> if i == i' then eval (C f g) i s'' else (Left i', s'')
Right a -> (Right a, s'')
Выполнение цепного правила несколько сложнее, однако на самом деле сводится просто к вычислению сначала одного действия, получению его результата и передачи этого результата во второе действие. Внимательный читатель может заметить, что здесь насамом деле написана какая-то ботва, потому что пространства маркеров возникающие при вычислении первого и второго действия пересекаются.
Вспомогательные функции реализуются элементарно:
put x = A (\s i -> (Right x, x))
get = A (\s i -> (Right s, s))
getCC = A (\s i -> (Right (A (\s' i' -> (Left (i+1), s'))), s))
Как легко видеть, getCC создает действие, которое пораждает другое действие, которое инициирует откат к маркеру следующему за маркером активным в момент вызова getCC. На самом деле, еще легче видеть, что это не столько похоже на get сurrent continuation, сколько на get label с последующим goto.
Изготовить из всего этого монаду еще проще
instance Monad (M s) where
return x = A (\s i -> (Right x, s))
f >>= g = C f g
В данной монаде, код приведенный выше работает, как и ожидалось, но как известно некоторые ответы пораждают дополнительные вопросы... Например, как заставить работать например вот такой код:
foo = do cc <- getCC
x <- get
put (x ++ ["foo"])
return cc
bar = do put ["bar"]
cc <- foo
cc
cc
cc
x <- get
return x
Основная проблема здесь в том, что числовой маркер не несет никакой информации о типе значения возращаемого действием на уровне, где это маркер был активен. А без такой информации как мне кажется, нельзя изготовить continuation, который будет возвращать этот результат. На ум просятся всякие shadow type, но я пока ни в чём не уверен.
Ах, да... Собственно к теме поста... В динамически типизированном языке такого (я имею ввиду взрывающие голову попытки засунуть тип в маркер) гемороя не было бы =)
---
* - Я прекрасно знаю о существовании статей типа A monadic framework for delimited continuations by Kent Dybvig, Simon Peyton Jones, and Amr Sabry, но не буду их читать, пока сам не разберусь в проблеме настолько на сколько меня хватит, такой у меня принцип.