Блог

Возможно ли создать тип с числовым аргументом?

т.е. если я хочу создать тип целых чисел с фиксированной разрядностью:

 newtype FixedWidth w = FixedWidth Integer

addFixedWidth :: FixedWidth w -> FixedWidth w -> FixedWidth (w 1)
mulFixedWidth :: FixedWidth w -> FixedWidth w -> FixedWidth (2*w)
  

Таким образом, средство проверки типов позволяет только FixedWidth добавлять или умножать значения одного и того же типа, но также определяет правильную точность результата.

Я знаю, что вы можете сделать что-то вроде этого:

 data Nil = Nil
data Succ x = Succ

addFixedWidth :: FixedWidth w -> FixedWidth w -> FixedWidth (Succ w)
  

и представить число 4 как Succ (Succ (Succ (Succ Nil)))) , но это невероятно уродливо. Мне также нужно выяснить, как добавить два Succ s для типа результата умножения.

Функция, которую вы ищете, — это естественные функции на уровне типов, известные как -XTypeNats расширение Haskell.

На данный момент это возможно только в экспериментальной ветви GHC. Я думаю, что это, вероятно, объединится с GHC к 7.4.

Некоторое дальнейшее чтение:

• TypeNats, вики-страница GHC.
• Естественные основы на уровне типов
• Билет # 4385.
• Ветвь TypeNats GHC