Это немного загруженный вопрос.
Галлина могла существовать независимо от OCaml, хотя, будучи лямбда-исчислением, она разделяет с ним некоторую конструкцию и семантику, и, будучи развитой в мире OCaml, она также разделяет некоторый конкретный синтаксис. Но OCaml не мог бы занять место Галлины.
Некоторые сходства:
- Они используют функциональный язык, основанный на лямбда-исчислении.
- Они имеют аналогичные описания алгебраических типов данных (хотя есть много различий в том, что допустимо и выразимо).
Некоторые (основные) различия:
- Gallina имеет зависимые типы, в то время как OCaml имеет систему типов, близкую к prenex-polymorphic System F с некоторым подтипом ... Я не уверен, как это назвать, но в некоторых он менее выразителен, чем зависимые типы кстати, хотя у него есть некоторые дополнительные функции, отсутствующие в Галлине.
- Галлина является полной, то есть все функции должны быть синтаксически корректными, либо явно завершенными, либо явно прогрессирующими в вычислениях. OCaml - это язык более общего назначения, для которого не подходит терминация.
- Галлина чиста, в то время как у OCaml есть побочные эффекты примитивов.
- Галлина «функциональна только», если хотите. OCaml имеет представление об объектах, некоторых «императивных» функциях (из-за всех перечисленных ранее отличий).
Фактически, исторически, ML (который OCaml является некоторым вариантом) был для LCF своего рода тем, что Ltac для Галлины! :-D (о боже, я мог бы получить некоторые злые комментарии из-за этой заметки ...)