Снова о статической типизации

Или есть функция, заведомо производящая значения данного типа.

ну и как, умея вычислять простые числа, установить, что число данное число простое?

или вот тип данных - «осмысленная фраза». как установить что данная фраза осмысленна, если вы умеете составлять осмысленные фразы. а вот никак не установить без функции, умеющей вычислять «осмысленность фразы».

как установить что данная фраза осмысленна, если вы умеете составлять осмысленные фразы

А чего тут устанавливать, если она осмысленна по построению?

осмысленна по построению

ее например ввел пользователь. или она была составлена по некоему алгоритму, и нужно понять - осмыслена ли она или нет. то есть проверить корректность ее присваивания в переменную типа - «осмысленная фраза».

В большинстве (да во всех почти) используемых в промышленности статически типизированных языков нет типа «целое число от 0 до 255». А это самое просто, чего только можно придумать. Что уж говорить о более сложных случаях?

В общем случае решения нет, а для частных можно придумать правила вида «арифмитические действия над действительными числами всегда дают действительное число и никогда комплексное», «синус/косинус любого угла всегда лежит в диапазоне (-1;+1)» etc. Только такие вещи, мне кажется, проще решить внешним анализатором, нежели насиловать штатную систему типов.

ну и как, умея вычислять простые числа, установить, что число данное число простое?

Считаем, что простые только те, которые мы вычислили. Про остальные ничего не известно.

как установить что данная фраза осмысленна, если вы умеете составлять осмысленные фразы

Если я её составил, как осмысленную, значит осмысленная.

В большинстве (да во всех почти) используемых в промышленности статически типизированных языков нет типа «целое число от 0 до 255»

byte есть практически везде.

И даже если нужен «целое число от 0 до 300», то везде легко строится через что-то типа

makeInt0_300 :: Int -> Maybe Int0_300
makeInt0_300 x = if x >= 0 && x <= 300 then Just (Int0_300 x) else Nothing

byte есть практически везде.

Только это не «целое от 0 до 255», а «кольцо вычетов по модулю 256». И то, что на это всем плевать, многое говорит о пользе статической типизации.

просто под «типизацией» часто имеют ввиду лишь форму представления, что является не вполне типизацией, а лишь одной из черт ея.

потому когда говорят «байт» - имеют ввиду 8 бит представления. а на строгости формулировок операций на этих битах кладут болт.

Только это не «целое от 0 до 255», а «кольцо вычетов по модулю 256»

В смысле? Значения — целые числа от 0 до 255. Операции с ними могут быть любые. Просто в большинстве случаев если не делать кольцо вычетов, то при переполнении надо вызывать исключение.

Или делать систему типов не хуже, чем в Liquid Haskell и Typed Racket.

Только это не «целое от 0 до 255»

Вот как раз оно самое и есть.

а «кольцо вычетов по модулю 256»

Кольцо по определению включает в себя определённый набор операций. Так вот байт не может быть кольцом. Байт с операцией суммирования по модулю - может быть. Но к байту можно применять также сумму с проверкой на переполнение или сумму с насыщением.

И то, что на это всем плевать, многое говорит о пользе статической типизации.

Под статической типизацией смешивают два понятия.

1. Указание типа переменной для скорости скомпилированной программы. Примеры: Си с наследниками.

2. Указание типа переменной для корректности программы. Примеры: *ML, Haskell, Agda, Typed Racket.

В первом случае тип выбирается под машинное слово и операции процессора. Отсюда кольцо вычетов и UB.

Во втором случае тип выбирается по требованиям задачи и там вполне нормально можно статически проверять, что не будет переполнения. Или что переполнение не забыли проверить и обработать.

makeInt0_300 :: Int -> Maybe Int0_300
makeInt0_300 x = if x >= 0 && x <= 300 then Just (Int0_300 x) else Nothing

ну так как записать множество простых в данной нотации?

то при переполнении надо вызывать исключение.

Да, надо. Если есть переменная типа «целое от 0 до 255», то при попытки записать туда 468, «468», 468.0, 468 + i*0, true, {value: 468} и т.п. надо вызывать исключение. Если это можно проверить на этапе компиляции, надо проверять на этапе компиляции. Мы строим всю программу вокруг типов, не для того, чтобы выяснить, что типы ничего не гарантируют и всё равно нужно следить за правильной интерпретацией битов и байтов.

А потом те же самые люди ругаются, когда мошенники в договорах важные вещи пишут в сносках супермелким шрифтом.

Вот как раз оно самое и есть.

Ноуп. Выше объяснил почему.

Но к байту можно применять также сумму с проверкой на переполнение или сумму с насыщением.

В промышленных языках такое можно только в динамике. Строгая динамическая типизация вещь очень полезная, тут никаких сомнений.

В первом случае тип выбирается под машинное слово и операции процессора. Отсюда кольцо вычетов и UB.

процессор следит за переполнением, там бит переноса имеется. как только он выставился - получилось переполнение. плюс семантика операции зависит от размера операнда.

то есть намахать любую арфиметику, хоть с кольцом, хоть без - это вопрос не машинно-ориентированности, а всего лишь соглашения об абстрактной машине, которое себе придумали разрабы языка.

Ноуп. Выше объяснил почему.

А я выше объяснил, почему таки да.

В промышленных языках такое можно только в динамике.

В смысле, складывать два числа только в динамике? В некоторых языках можно написать операции суммирования, возвращающие число гарантированно того же диапазона, либо ошибку. В ещё более ограниченном кругу языков можно написать доказательство, что число действительно будет из этого диапазона, а не просто положиться на реализацию.

Строгая динамическая типизация вещь очень полезная

Это как в питоне-то? Предпочитаю статическую.

в js нет тредов. поток всего один, а worker_threads это скорее резиновая женщина, а не поток. поэтому кошерных мьютексов в джиесе нет и быть не может. в js/ts есть async/await зато. и поэтому в JS mutex выглядел бы как-то так.

class Mutex {
  constructor() {
    this.queue = [];
    this.locked = false;
  }

  lock() {
    return new Promise((resolve) => {
      if (this.locked) {
        this.queue.push(resolve);
      } else {
        this.locked = true;
        resolve();
      }
    });
  }

  unlock() {
    if (this.queue.length > 0) {
      const nextResolve = this.queue.shift();
      nextResolve();
    } else {
      this.locked = false;
    }
  }
}

// Usage example
const mutex = new Mutex();
const sharedResource = { value: 0 };

async function modifyResource() {
  await mutex.lock();
  try {
    // Critical section
    sharedResource.value++;
    console.log(`Resource value: ${sharedResource.value}`);
  } finally {
    mutex.unlock();
  }
}

// Simulate concurrent modifications
modifyResource();
modifyResource();
modifyResource();

НО! задачу ОПа это не решает. И JS никогда ее не решит. Потому что то что написано выше, это не мьютекс, а кал говна как и сама задача. Потому что в динамических языках мутировать переменные, а еще и асинхронно - это большой харам. некоторые конфиги линтера вообще настраивают так чтобы let нельзя было использовать и нельзя было присваивать свойства к объекту на лету (aka monkey patching).

В смысле, складывать два числа только в динамике?

Проверять значение сложения чисел можно только в динамике → проверять результат на нахождение в заданном диапазоне можно только в динамике → проверять на принадлежность типу можно только в динамикее → у вас динамическая типизация.

В ещё более ограниченном кругу языков можно написать доказательство,

Да, зависимые типы это могут. Но они не могут в промышленное программирование. Это уже обсуждалось выше.

Проверять значение сложения чисел можно только в динамике

Ну да, есть число a :: I320 и число b :: I320. Как кроме как в динамике проверить, что результат (a + b) :: I320?

проверять результат на нахождение в заданном диапазоне можно только в динамике

Вот именно. И никакие зависимые типы не помогут.

проверять на принадлежность типу можно только в динамике

Нет, проверять, можно ли значению присвоить желаемый тип, можно только в динамике. Банально, спросили у пользователя номер порта, и проверить, что он не написал «чиво?», можно только в динамике. Но как-то же программа в итоге имеет свой uint16?

у вас динамическая типизация.

Любой ЯП имеет динамическую типизацию, ясно-понятно.

Банально, спросили у пользователя номер порта, и проверить, что он не написал «чиво?», можно только в динамике.

Если мы пишем

unsigned char a = 177;
unsigned char b = 200;
unsigned char c = a + b;

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

Во-вторых, … //тут скучно, поэтму пропустим.

А, в-третьих, да, самые важные и интересные проверки можно сделать только в динамике, поэтому проще не лохматить бабушку, а сразу перейти под стяг динамической типизации.

Любой ЯП имеет динамическую типизацию,

Да.

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

Если сделать так, то все арифметические операции станут в несколько раз медленнее (+ один условный переход на каждую).

Также. Либо makePrime :: Int -> Maybe Prime, который проверяет переданное число. Либо genPrime :: SomeData -> Prime, про который достоверно известно, что он генерирует простые числа.

А, в-третьих, да, самые важные и интересные проверки можно сделать только в динамике, поэтому проще не лохматить бабушку, а сразу перейти под стяг динамической типизации.

главные проверки типов, это не арифметика, а вызовы функций, методов, подстановка параметров. и при статической типизации это делается при компиляции, а при динамической - понятно когда.

вызовы функций, методов, подстановка параметров. и при статической типизации это делается при компиляции

я тоже топлю за статическую типизацию, но все равно найдется чемодан который скастит тип и скажет что так и надо

который проверяет переданное число

и будет его проверять примерно миллион лет. и что делать? можно ли это считать вполне точным определением типа данных?

Так на этапе компиляции же проверять, данный кода вообще не скомпилируется, а потому будет абсолютно быстрым.

Так на этапе компиляции же проверять, данный кода вообще не скомпилируется, а потому будет абсолютно быстрым.

Я имею в виду тривиальное

unsigned f(unsigned a, unsigned b, unsigned c)
{
  return (a+b)*c*2+3;
}

Если нельзя оборачивать через 0, то здесь будет четыре условных операции. И если вдруг шаблон разворачивается в a+b-b, то нельзя заменять на a, надо вычислять сумму и проверять на переполнение.

и будет его проверять примерно миллион лет. и что делать?

Не использовать создание из произвольного числа для таких больших чисел. Если массив такого размера сделать и нулями заполнить, это тоже миллион лет займёт. Это же не повод не пользоваться массивами.

можно ли это считать вполне точным определением типа данных?

Конечно. Математически всё однозначно.

Не использовать создание из произвольного числа для таких больших чисел.

число в 150 десятичных знаков надо факторизовать черти сколько лет. 150 байт всего-то.

число в 150 десятичных знаков надо факторизовать черти сколько лет. 150 байт всего-то.

А без типов как будешь проверять? Вот у тебя питон, пользователь ввёл эти 150 знаков, а заказчик хочет, чтобы введённые простые числа были записаны.

Система типов может гарантировать только, что если ты пообещал (в ТЗ) записывать только простые числа, то что будет гарантия, что в функцию записи попадёт число, которое либо было проверено, что оно простое, либо было получено из функции, про которую ты пообещал (описанием функции), что она всегда возвращает простые числа.

Очень помогает от ошибок по невнимательности.

самые важные и интересные проверки можно сделать только в динамике, поэтому проще не лохматить бабушку, а сразу перейти под стяг динамической типизации.

Ну да, вместо проверки, что строка input_str содержит номер порта и конвертации оной в u16, будем везде таскать input_str как есть и делать проверки при каждом использовании.

Я таки поддержу анонимуса с матаном.

Беда в том, что типов обычно не хватает.

Ну, выразимость зависимых типов эквивалентна выразимости логик высших порядков. Т.е. всё что можно выразить в логике, можно выразить и в зависимых типах, было бы желание.

Или человек при описании типа забыл существенное условие.

Тут ситуация точно как с формулировками теорем в матане. Т.е. конечно бывают ошибки в формулировках лемм/теорем. Бывают менее удобные/более удобные формулировки. Всё это понятно. Но в основном, если человек в теме, то формулировки он обычно без проблем читает и вполне понимает правильные они или нет в подавляющем большинстве случаев.

Ну, выразимость зависимых типов эквивалентна выразимости логик высших порядков. Т.е. всё что можно выразить в логике, можно выразить и в зависимых типах, было бы желание.

Напиши тип для mapcar. Если язык не позволяет произвольное число аргументов, то пусть списки будут в кортеже.

Чтобы работало

mapcar (\s x -> s ++ show x) (["aaa", "bbb"], [1, 2]) == ["aaa1", "bbb2"]

mapcar (+ 1) ([1, 2]) == [2, 3]

для любого количества элементов в кортеже.

Вы сейчас что-то на своей волне вещаете.

Но в основном, если человек в теме, то формулировки он обычно без проблем читает и вполне понимает правильные они или нет в подавляющем большинстве случаев.

Я не про это. Есть классическая задача для собеседования: «Нужно протестировать консольное приложение, которое на вход принимает 3 целых числа, интерпретируемые как длины сторон треугольника, а на выходе выводит на экран является ли введенный треугольник равнобедренным или равносторонним.». Люди забывают проверить на то, что это вообще треугольник. Забывают проверить, что равнобедренных три варианта.

Если ты в типе напишешь РавнобедренныйТреугольник == Треугольник a b c | b == c, а потом в проверке то же самое, контроль типов тебя не спасёт.

вполне понимает правильные они или нет

Когда ТЗ хоть немножко нетривиальное, то выяснить, совпадает ли тип с тем, что имел в виду заказчик, задача достаточно сложная. Причём, если тестами можно заставить заказчика согласиться или не согласиться с тем, что понимание верное (относительно результатов тестов), то описание типа для заказчика обычно слишком сложно для понимания.

Интересно, будет ли хотя бы 20 страниц?

P.S. Раскрою.

Ну да, вместо проверки, что строка input_str содержит номер порта и конвертации оной в u16,

Динамическая типизация не запрещает нам преобразовывать строку в число, даже странно что вас натолкнуло на такую мысль. Но дело даже не в этом. Номер порта как u16 — это скучно, банально и почти бесполезно. Для начала порты бывают двух видов: привелегированные (от 0 до 1023) и непривелегированные (от 1024 до 65535). И это важно, с точки зрения использования программы. Если тип данных [1024;65536] в вашей системе типов непредставим, то и дальнейшую пользу от статической типизации вы получить не сможете, всё равно придётся обмазываться динамическими проверками.

Т. Е. Функции mapcar мы передаем 1) Функцию f, 2) произвольное число списков n. При этом функция f должна принимать n аргументов (по одному из каждого списка). Ну и результат есть список результатов применения функции к соответствующим элементам аргументов?

Кажется решаемым, если так. Сейчас не за компьютером, как доберусь - попробую написать.

Мне кажется или это похоже на аппликативный функтор, только в список обёрнутый как то?

Не, запал не тот по моему. Вяленько...

Нет, ну погоди. Давай отделим мух от котлет. 1) заказчик и типы, это интересно,конечно. Но это что то нетрадиционное. Давай сразу оставим на потом.

2) ну понятно что можно облажаться. Ну так и без типов человек так же облажается с треугольником.

На мой взгляд смысл в том что типы читать и писать обычно много проще чем код. А типы гарантируют написание правильного кода. Ну, более-менее правильного в общем случае.

А ладно....

Зависимые типы прекрасно могут в промышленное программирование.
https://hh.ru/search/vacancy?text=Scala&from=suggest_post&salary=&amp...

То что некоторые бедолаги не могут вытащить голову из одного места и предпочитают смотреть на говно мамонта в новой упаковке как на большущую инновацию, это уж извините, не вина зависимых типов.

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

Искренне желаю успехов.

Хотя...

У нас, у обезъян это называется array_map(). При желании туда можно и лямбду засунуть.

У нас лямбды раньше так страшно выглядели (а до этого их совсем не было, емнип) , что нужно было иметь очень горячее желание чтобы их туда засунуть. Не знаю поменялось ли что нибудь с тех пор.

К слову, моё предыдущее место работы, стартап небольшой, как раз использовал Scala. Жаль, по миру пошёл из-за финансовых причин. Так бывает, технологии клёвые, а продаж мало.

Так бывает, технологии клёвые, а продаж мало.

Как замечательно, что вы провели этот пример! Это так много сразу прояснило! Мне, например, стало совершенно
очевидно, что проблема была в зависимых типах. Еслиб на пхп писали, продажи бы конечно были до небес. И сразу, что важно.

Пацаны, короче, тут всё ясно, расходимся.

Я про скалу, между прочим, ничего плохого не говорил. Если б и хотел ругаться, то напал бы на sbt — simple build tool, для того, чтобы понять в какой последовательности и как собирается проект, достаточно вообразить себя пятимерный гиперкуб, каждый этап сборки — это точка в данном кубе, а весь сборочный процесс образует соответствующую гиперплоскость.

Я про скалу, между прочим, ничего плохого не говорил.

Ну, скала - язык с зависимыми типами. Что противоречит тезису «зависимые типы не могут в промышленное программирование».