Мысли вслух.

[thesz]

Думаю над всякими зависимыми типами.

Epigram под виндами не завелся, макинтош все ремонтируют, а линукс ставить неохота.

Поэтому буду фантазировать.

Сперва - определение самих типов данных. В стиле алгебраических типов Хаскеля.

Общий вид таков (подчеркнутое - ключевое слово или часть синтаксиса, зачеркнутое может отсутствовать, {x}n - выражение x, повторенное n раз, n=* - 0 и более раз, n=+ - 1 и более раз):
data typrecond => conid tyvarslist =
typrecond => conid tyexprlist {| typrecond conid tyexprlist}*;Как-то так.

В typrecond к названию типа мы указываем общие ограничения на используемые внутри переменные. Затем они (эти переменные) перечисляются в качестве параметров типа (после первого conid). Ограничения наподобие x:* (x - любой тип) можно опустить.

Далее у нас идет объявление списка вариантов, разделенных |.

К каждому варианту мы можем добавить дополнительное ограничение. Сами варианты могут содержать выражения типов.

Вот, например:
data Bool = False | True ;

data List x =
Nil
| Cons x (List x)
;

{- Альтернативная запись:
data x : * => List x =
Nil
| xs::List x => Cons x xs
;
-}

data Nat =
Zero
| Succ Nat

data Integer = Integer (List Bool)

-- А что бы мне и функцию не объявить?
length :: (list :: List *) -> Integer = rec list of
Nil -> 0
Cons _ xs -> 1+length xs

{- Вариант:
length :: instance Num x => (list :: List *) -> x = rec list of
Nil -> 0
Cons _ xs -> 1+length xs

Указав instance conid tyexpr, мы указываем на группу ограничений:
class Num x where
exist fromInteger :: Integer -> x
exist (+) :: x -> x -> x

class Eq x where
exists (==) :: x -> x -> Bool

Такого плана.

Что здесь будет твориться с сообщениями об ошибках...
-}

-- интересно, можно ли этот кусочек сделать выводимым?..
integerBits (Integer bits) = bits

data Int32 =
x :: Integer, length (integerBits x) == 32 => Int32 x
Как-то так.

Синтаксис смешанный, где двумерный, где обычный. Потом разберусь.

Вроде, не совсем ужасно и даже кое-где понятна логика работы.