Система взаимодействия ocaml использует унификацию. Вы можете считать это вычислительным устройством, и в этом случае у него есть чувство логического программирования. Но возможности довольно ограничены, поскольку это никогда не было одной из целей системы типов. Как вы увидите на странице, предложенной Джеффри, вычисления на уровне типов посредством объединения на самом деле довольно ограничены (трудно выразить, например, умножение). У Haskell есть более мощный язык ограничений, но опять же, я не уверен, что логическое программирование в системе типов - хороший способ.
Другая часть системы типов OCaml может выполнять вычисления на уровне типов в своем модуле и языке функторов. Функторы позволяют выражать вычисления на уровне типов в разновидности, связанной с формальным языком программирования Fω. Возможно, вы могли бы кодировать церковные цифры на уровне типов в языке модуля, но я не вижу, что вы могли бы сделать с этим, так как кажется, что довольно трудно получить результаты в полезной, пригодной для использования форме. В частности, я не понимаю, как превратить информацию о типе обратно в значения, используемые вашей программой, как это делают C ++ или D с помощью вычисления констант во время компиляции.
Так что да, система типов OCaml (и наиболее функциональный язык, который будет содержать SML, Haskell и Scala) также обладает некоторой вычислительной мощью, но нет, я бы не ожидал, что она будет особенно полезной предварительный расчет с ними; и это, конечно, не стандартная практика среди программистов OCaml. Типы лучше всего рассматривать как типы, которые дают статические гарантии относительно значений, которые они классифицируют.