История изменений
Исправление hateyoufeel, (текущая версия) :
Так у класса типов значения не бывает.
Да, потому что это constraint. Но я не об этом. Я о том, чтобы вынести значение из типов образно в значения, как например knownNat это делает с числами.
У любого значения в Haskell только один тип.
В Haskell – да. Но если мы добавляем Refinement Types, то это уже далеко не так, и каждое значение может пренадлежать какому угодно количеству этих refined types.
Ну и да, я всё ещё утверждаю, что dependent types и refinement types – разные вещи, у которых только области применения слегка пересекаются.
Исходная версия hateyoufeel, :
Так у класса типов значения не бывает.
Да, потому что это constraint. Но я не об этом. Я о том, чтобы вынести значение из типов образно в значения, как например knownNat это делает с числами.
У любого значения в Haskell только один тип.
В Haskell – да. Но если мы добавляем Refinement Types, то это уже далеко не так, и каждое значение может пренадлежать какому угодно количеству этих refined types.