Сабтайпинг для индуктивных типов

Предлагается трактовать обозначения [T :> Nat] и [T <: Nat] как [T : NNO] и [T : CoNNO] соответственно, где
@Structure NNO:
  @on N : Type
  zero : N
  succ : N -> N

@Structure CoNNO:
  @on N
  rec[T : NNO](n : N) : T
  rec[:T](zero) = T.zero
  rec[:T](succ(:n)) = T.succ(rec[T](n))

Отметим, что если N1 N2 : NNO ∧ CoNNO, то между типами N1 и N2 имеется изоморфизм, причём каноническим представителем этого класса эквивалентности типов является
@Family Nat:
  zero : Nat
  succ : Nat -> Nat

Для любого индуктивного типа IndT можно автоматически генерировать структуры IND-T и CoIND-T, таким образом проясняя что подразумевается под [T :> IndT] и [T <: IndT]. Наличие таких обозначений позволяет в общем виде описать тип рекурсора для любых индуктивных типов:
IndT.rec[X <: IndT <: Y](x : X) : Y

( Read more... )

Okmij

Вчера у меня наконец дошли руки посмотреть на статью Freeer monads Олега Киселёва et al., и реализацию — библиотеку Eff для хаскеля. Вот блин, а. Это же надо так уметь. Шедевр, тончайшая работа.

На чистом хаскеле безо всяких макросов превратили его фактически в язык с модулярными алгебраическим эффектами. Описываешь свой эффект как в языках с алгебраическим эффектами через параметризованный GADT, т.е. просто пишешь какие ты хочешь добавить в ambient language команды с описанием их сигнатуры, пишешь ему модулярный интерпретатор, а дальше можно это свободно перемежать с другими описанными в такой же форме эффектами, умная бубиотика определяет параметрическую монаду Eff '[list of effects], всё настолько круто, что там не только композиция эффектов работает сама и полиморфные по эффектам процыдурки сами получаются, но даже effect inference для do-нотации в какой-то мере работает. И семантически очень красиво выходит: алгебраическое описание эффекта это индуктивный тип * -> *, для него конструируется левое расширение Кана, а на получившемся функторе задаётся свободная монада, вложение индуктивных типов превращается во вложение монад, соответственно “описания эффектов” можно комбинировать через disjoint sums, прощайте монадные трансформеры. В библиотеке описаны стандартные эффекты — IO, State, Non-Determinism, и всё что можно описать через Delimited Continuations (эксепшены, кооперативный мультитрединг/сопроцедуры и т.д.).

Заодно понятно, каким образом будет выглядеть комбинирование эффектов с зависимыми типами. Кажется, там ничего не сломается, кроме того что Eff станет вообще говоря относительной монадой (“монадоподобный объект, не являющийся эндофунктором”). Единственное, что мне пока не понятно — это как в сигнатуре эффекта указывать соотношения (например требовать, чтобы вызовы ReadEnv коммутировали), я вообще пока не встречал удовлетворительного подхода к этому вопросу, если работать в терминах монад/комонад, а не в терминах стрелок. Но по идее оно должно быть, собственно монадами описываются эффекты, у которых контракты накладываются на интерпретатор (если он есть), а процедуры могут полагаться на их выполнение, а комонадами эффекты, налагающие на использующую их процедуру обязательства по выполнению контрактов (например, использовать вызов команды только один раз).