DP
И аналогично для других типов, если для всех определён дефолт
Size: a a a
Типы в языках программирования, моделирования, представления знаний и жизни
505 membersпожаловаться на группу
2022 January 24
AC
Это и есть синтаксический сахар. 😊
AC
Так проще всего.
Можно, конечно, добавить отдельно в операционную (или ещё какую) семантику, но тогда лишние правила будут мешаться в доказательствах типа soundness.
Можно, конечно, добавить отдельно в операционную (или ещё какую) семантику, но тогда лишние правила будут мешаться в доказательствах типа soundness.
АП
хм.. вопрос:
Если
Получается что в компайл-тайме перезаписывается значение для v ?
То есть сначала
Если
v :: Natрассахаривается в
v :: Nat = 0то что происходит когда я пишу
v :: Nat?
v = 3
Получается что в компайл-тайме перезаписывается значение для v ?
То есть сначала
v :: Natрассахарится в
v :: Nat = 0в результате чего v становится равным 0, а после обработки
v = 3v становится равным 3.
K
Это язык-то какой? Если хаскелль, то
v :: Nat без v = 3 это ошибка компиляцииАП
Ну я говорю о гипотетическом языке, в котором
v :: Natрассахаривается в
v :: Nat = 0АП
это может быть и хаскель, но с указанным сахаром
K
Лично я против дефолтных значений в определениях и мутаций вне выделенных переменных, так что ничего не подскажу
DP
v :: Nat
v = 3
можно также преобразовать в
v :: Nat = 3
v = 3
можно также преобразовать в
v :: Nat = 3
gо
ну, можно рассахаривать
без определения в
где
val :: Type
без определения в
val :: Type
val = default
где
class Default a where
default :: a
gо
если ты действительно хочешь дефолтное значение, то не так сложно написать
а если ты случайно пропустил / удалил / потерял при мёрдже строчку с определением, то ты хочешь ошибку компилятора
val = default
а если ты случайно пропустил / удалил / потерял при мёрдже строчку с определением, то ты хочешь ошибку компилятора
a
2 раза перечитал диалог так и не понял, почему v :: Nat = 0?
DH
Мне кажется это надо в цитаты
E
ага, учитывая, что в одной из математических школ натуральный ряд чисел вообще не включает ноль
[
...когда надо v :: Nat = fix S
a
v :: f v = fix v
точнее
точнее
a
добро пожаловать в идт