вівторок, 8 жовтня 2013 р.

Безопасный void* на Agda

В стандартной библиотеке Хаскеля есть тип Dynamic, который состоит из значения, тип которого как-бы утрачен, и тега, который представляется типом TypeRep. TypeRep — это по сути дерево из строк, среди которых есть имя пакета с версией, имя модуля, имя самого типа, и так для всех составляющих. Его можно использовать как уникальный идентификатор типа. Так он и используется в Dynamic, если TypeRep'ы одинаковы, unsafeCoerce'им.

Это конечно все очень удобно, но больно напоминает void*. По сути оно таким и является, даже похоже менее безопасным чем C++ RTTI (поскольку TypeRep можно задать самому, а к C++ typeid прямого доступа нет). Ну и как водится решил я написать такой TypeRep, который позволил бы безопасно делать то же. На Хаскеле сразу не получилось, по этому решил написать прототип на Агде. Круто:) на Агде пишем прототипы для Хаскеля. Заодно пришлось написать платформу для эмуляции Хаскельных type class'ов на Агде.

Вот что у нас получилось. Во-первых нужно задать контекст: это те конструкторы типов которым мы разрешаем присутствовать в используемых нами типах (не всех конечно, а только заворачиваемых в Dynamic).

CTX = String ::: List ::: List  ::: []

То есть у нас могут присутствовать строки, списки строк, списки списков строк, списки чисел, списки списков чисел, и т.д.; просто числа быть не могут. Обратите внимание на типы этих конструкторов — они могут быть разные (*, * -> *, (* -> *) -> *, и т.д.). То есть, контекст — это гетерогенный вектор конструкторов типов. С этим у меня возникли проблемы на Хаскеле.

Ниже функция которая принимает запакованный тип и пробует привести его либо к строке либо к списку чисел. И в зависимости от типа делает разные вещи.

go : Dynamic CTX  String
go dyn = maybe id fallback
         (showℕ  sum <$> cast< List  > dyn 
          cast< String > dyn)
  where
    fallback = "Value is neither String nor List ℕ"

Тестируем все это дело.

test-string : go (toDyn CTX "I'm String")  "I'm String"
test-string = refl

test-list : go (toDyn CTX (downFrom 10))  "45"
test-list = refl

Так выглядит тип Dynamic. Как видите, внутри сохраняется тип, значение, и представление типа, которое и позволяет сравнивать типы (на код можно посмотреть сюда). Ниже функция которая запаковывает любое значение, для которого можно построить представление (BuildTypeRep), в Dynamic. Синтаксис похож на используемый для классов типов в Хаскеле, но это (=>) всего лишь самодельный оператор. (Кстати мощность этих самодельных классов не уступает Хаскельным даже с расширениями.)

record Dynamic {} {n} (vec : Vec (Heterogeneous (suc)) n) where
  constructor dynamic
  field
    typ : Setval : typ
    rep : TypeRep vec {Set} typ

toDyn :  {} {n} (vec : Vec (Heterogeneous (suc)) n)
        {typ : Set} (val : typ) 
        BuildTypeRep vec typ => Dynamic vec
toDyn _ val = withI λ i  dynamic _ val (BuildTypeRep.get i)

А вот так выглядит каст. Хочу напомнить, что Агда не терпит противоречивости, по этому в ней нет unsafeCoerce. То есть все четко, правильно и безопасно; короче приложение не упадет из-за каста. Я понимаю что в Хаскеле и даже С/С++ тоже можно гарантировать, что не упадет, но эта гарантия 99.9% (или 85% в случае С++ :-D), до тех пор пока кто-то чего-то не забудет. А данный подход дает 100% гарантию, компилятор просто не позволит сделать неправильно, так как тип гарантирует безопасность.

cast<_> :  {} {n} {vec : Vec (Heterogeneous (suc)) n}
          (typ : Set) (dyn : Dynamic vec) 
          BuildTypeRep vec typ => Maybe typ
cast< typ > dyn = withI λ i  _

Писать эту прелесть было очень интересно, поскольку походу возникло множество интересных задач, как на понимание, так на разработку новых подходов. Описать за один раз как эта шутка работает не представляется возможным. Но за несколько — все реально:) А для нетерпеливых тут код.

Немає коментарів:

Дописати коментар