Как бы вы это ни назвали, на типизацию это никак не повлияет, она как была статической, так и осталась, так как в процесс типизации при написании модулей вмешиваться не надо.
Более подробен комментарий выше моего. Суть в том, что благодаря упомянутому изоморфизму, утверждение «x > y» — это такой тип. Если у него есть хотя бы одно значение, значит утверждение верно. Например, у типа «1 > 0» есть значение. Вот код на Агда:
-- натуральное, например Succ (Succ Zero) - это 2
data Nat : Set where
Zero : Nat -- ноль
Succ : Nat → Nat -- n + 1
-- тип, утверждение, что одно число не меньше другого
data _≥_ : Nat → Nat → Set where
-- любое число больше нуля
≥Zero : {n : Nat} → n ≥ Zero
-- если n ≥ m, то n + 1 ≥ m + 1
Succ≥Succ : {n m : Nat} → n ≥ m → Succ n ≥ Succ m
proof₁ : Succ Zero ≥ Zero -- 1 ≥ 0
proof₁ = ≥Zero -- доказали
proof₂ : Succ (Succ Zero) ≥ Succ Zero -- 2 ≥ 1
proof₂ = Succ≥Succ proof₁ -- тоже
Таким образом, упомянутая функция помимо двух чисел принимает доказательство того, что одно из них больше другого. Доказательство можно либо вывести из чего-либо, либо получить «нахаляву» внутри одной из веток if. Т.е. внутри then у нас есть значение типа x < y (в примере на Idris: LT x y), ну а внутри else есть доказательство отрицания этого утверждения.
Т.е. строго говоря не «в ветке x и y удовлетворяют типу функции», а «в ветке есть значение-доказательство требуемого утверждения — что x < y».
Вот это «наличие удобной работы» и есть тот «отдельный рантайм», про который я говорю.
Если сделать в Хаскеле нормальный Dynamic, который помимо метки типа будет таскать словарь со служебными функциями, то рантайм писать не надо, надо написать модули для работы с этим в рамках текущего рантайма. Возможно, я что-то не учёл?
Служебные функции типа to_str, op_equal и т.п., чтобы реализовав их для своего кастомного типа, его можно было бы сразу класть в Dynamic и орудовать им. Ибо сейчас в Dynamic можно положить любой Typeable, но с ним можно не глядя сделать только одно — попробовать конвертнуть в заданный тип. Если потребовать класть словарь с кучей функций, то можно будет складывать, преобразовывать в строку, сравнивать и т.п.
Могу даже попробовать на досуге реализовать такой Dynamic, если есть интерес, вдруг я что-то не учёл.
Введение Dynamic в Хаскель не сделало его динамическим:
let x = dynApp (toDyn (*20)) (toDyn 10)
let y = dynApp (toDyn negate) x
let z = dynApp (toDyn (show :: Integer -> String)) y -- стандартный show не умеет в динамику
let x' = fromDynamic x :: Maybe Integer -- Just 200
let y' = fromDynamic y :: Maybe Integer -- Just -200
let z' = fromDynamic z :: Maybe String -- Just "-200"
let k = dynTypeRep z == typeRep (Proxy :: Proxy String) -- True, тип String
Другое дело, что чтобы этим было удобно пользоваться, надо написать дополнительные модули, но технически это можно сделать. Конкретно Хаскельный Dynamic для этого плохо приспособлен (его задачи проще — конвертнуться туда-обратно, а не работать напрямую с ним), так как там только метка типа и всё, а было бы хорошо туда положить ещё служебных функций (show, op_plus, op_equal...).
Собственно, если прикрутить soft types, при котором стандартный вывод типов иногда выводит Dynamic, это (наличие удобной работы) становится необходимым. Система типов же от этого не становится динамической, все типы известны статически, иногда это any/dynamic. При динамике же у всех переменных статически один тип — any/dynamic.
В языке по ссылке при отсутствии определённых конструкций типа
if cond then 1 else "blah"
все типы выведутся и всё будет статическим. Какой же он динамический-то?
Посмотрите, какой тип он выводит так такой штуки — функции, проверяющей, что поданная на вход функция (с любым кол-вом аргументов) всегда вернёт true на любом входе.
taut = λB . case B of
true : true
false : false
fn : ((and (taut (B true))) (taut (B false)))
taut : β → (true + false) where
β = fix t . (true + false + ((true + false) → t)) -- рекурсивный тип
Если упростить тип для понимания, то он такой:
taut : β → bool where
β = bool | bool → β -- либо bool, либо bool → bool, либо bool → bool → bool, либо...
Кстати, немного оффтоп, есть такой канонический пример нетипизируемого лямбда-выражения:
λx. (x x)
В Agda, например, его можно типизировать:
S : {a : Set} {β : Set → Set} → ({α : Set} → α → β α) → β (a → β a)
S x = x x
id : {a : Set} → a → a
id x = x
test : {a : Set} → a → a
test = S id
Вы статью почитали? Язык, приведённый там — он со статической или динамической типизацией?
Если «построить отдельный рантайм» с нужными свойствами, получится язык со статической или динамической типизацией?
Тип any — это в тайп-скрипте, который всего лишь типизированный препроцессор к динамическому языку?
Да, но обобщить несложно, не так ли?
Тип Dynamic и в Хаскеле есть, к примеру. Другое дело, что там им неудобно пользоваться, но это уже ортогональный вопрос.
Вот посмотрите также на Soft types для ML-like языка.
Совсем вкратце про soft types: добавляются дополнительные правила вывода. В некоторых конкретных случаях при ошибке вывода выводится dynamic/any. Typescript, собственно, вроде как раз soft types и есть, просто он совместим с JavaScript, что накладывает ограничения. В статье приводится ML-like статический язык с такими же особенностями.
Доказав это на этапе компиляции тем или иным способом.
Например, для положительного числа x, пришедшего по сети, число x*2 + 1 всё равно больше, чем x, и такую пару можно передать без проверок.
Если же про оба числа ничего неизвестно, то, понятно, надо сделать динамическую проверку руками до вызова функции. Например, так:
if x < y then ... тут x < y, можно звать функцию ... else ... а тут нет ...
Ну на самом деле проблема несколько в другом. Я, например, смогу объяснить, но это требует усилий, чтобы пользоваться не привычным понятийным аппаратом, а тем, который понятен собеседнику. Ему действительно настолько интересно, что трата моих ресурсов на объяснение будет оправдана? Нередко ведь спрашивают «так, разговор поддержать».
Конечно, приходилось говорить много и с большими экскурсами, но если вам не нравится рассказывать, чем вы занимаетесь — вы занимаетесь чем-то не тем.
С этим абсолютно не согласен. Зачем рассказывать о том, чем занимаешься? Мне достаточно того, что мне нравится, чем я занимаюсь.
Мысленно добавьте перед сообщением «нет, ». К тому же аналогия неверная, они не сделали curl и wget, нет у МС такой программы, это алиас, который работает только внутри powershell. Это как если в языке программирования назвать некую команду wget'ом (кстати, нет чего-то такого в perl'е например?).
Осталось вам понять, что исходная команда, и «команда, записанная правильно» — разные команды. Одна работает, а другая — нет. Или вы всерьёз считаете, что это одна и та же команда?
Его конкретный пример команды — обоснование того, почему не работает и не будет работать исходная.
Команда работает, будучи записанной правильно, дорогой друг. :)
А правильно — это как? Так, чтобы работала? Ну тогда любая команда работает, если её правильно написать, но это уже какое-то альтернативное толкование слов.
Да зачем же?? Дорогой товарищ, вы, возможно, не заметили, но лично я в этой (под?)ветке обсуждал с Krey — не с Вами! :) — «неработу» find с опцией maxdepth 0.
И это всё. :)
По-моему, это вы так и не заметили, что с Krey вы обсуждали именно то, о чём пишу я, от этого у вас такое недопонимание сначала его, а потом и меня. Не верите, спросите его лично, он вам подтвердит. Или хотя бы обратите внимание на его ответ мне, где он подтверждает мои слова.
P.S.Команда таки работает — правда, только будучи записанной правильно. Но, как Вы и просили, я больше о Вашей команде ничего писать не буду.
И я вас прошу, не надо в очередной раз мне писать, какие стоит указать другие параметры (а значит и использовать другую команду), я с этим разобрался ещё с первых сообщений и прекрасно понимаю, почему find работает именно так, и какими способами можно поставленную задачу решить. Это не отменяет того факта, что исходная команда этого не делает. Вот она исходная, ещё разок:
Это уже просто не смешно. Прочтите наконец всю ветку от начала и до конца.
Я вам помогу. Ветка началась с этих сообщений:
Линукс, такой линукс. Решил проверить эту «команду», состоящую из запуска одной программы с параметрами. Не работает.
Пользователь линукс выложил на обозрение неработающую команду. Причем такую, что ни один пользователь НЕ линукса и многие пользователя линукса не поймут что она не работает пока не запустят. maxdepth=0 ассоциируется с тем что
Во всей ветке речь идёт именно о том, что не работает команда, а не программа. И под не работает подразумевается именно что, что это и значит — не делает то, что задумано. Я вам даже процитирую, что было задумано:
Отобрать все файлы, созданные не раньше 222 дней назад, запись в которые осуществлялась до 7 июля 2016 года, размер которых меньше 2ГБ, плюс к ним те, которые содержат в своем имени шаблон «bak».
А теперь будьте добры, покажите, где шла речь о том, что не работает программа find.
Не утилита find нерабочая, а вся целиком эта команда (find — не команда), так как она не делает то, что просили. Работоспособность и корректность самого find никто не оспаривал.
Таким образом, упомянутая функция помимо двух чисел принимает доказательство того, что одно из них больше другого. Доказательство можно либо вывести из чего-либо, либо получить «нахаляву» внутри одной из веток
if. Т.е. внутриthenу нас есть значение типаx < y(в примере на Idris:LT x y), ну а внутриelseесть доказательство отрицания этого утверждения.Т.е. строго говоря не «в ветке x и y удовлетворяют типу функции», а «в ветке есть значение-доказательство требуемого утверждения — что x < y».
Если сделать в Хаскеле нормальный Dynamic, который помимо метки типа будет таскать словарь со служебными функциями, то рантайм писать не надо, надо написать модули для работы с этим в рамках текущего рантайма. Возможно, я что-то не учёл?
Служебные функции типа to_str, op_equal и т.п., чтобы реализовав их для своего кастомного типа, его можно было бы сразу класть в Dynamic и орудовать им. Ибо сейчас в Dynamic можно положить любой Typeable, но с ним можно не глядя сделать только одно — попробовать конвертнуть в заданный тип. Если потребовать класть словарь с кучей функций, то можно будет складывать, преобразовывать в строку, сравнивать и т.п.
Могу даже попробовать на досуге реализовать такой Dynamic, если есть интерес, вдруг я что-то не учёл.
На систему типов это не влияет.
Dynamicв Хаскель не сделало его динамическим:Другое дело, что чтобы этим было удобно пользоваться, надо написать дополнительные модули, но технически это можно сделать. Конкретно Хаскельный Dynamic для этого плохо приспособлен (его задачи проще — конвертнуться туда-обратно, а не работать напрямую с ним), так как там только метка типа и всё, а было бы хорошо туда положить ещё служебных функций (show, op_plus, op_equal...).
Собственно, если прикрутить soft types, при котором стандартный вывод типов иногда выводит Dynamic, это (наличие удобной работы) становится необходимым. Система типов же от этого не становится динамической, все типы известны статически, иногда это any/dynamic. При динамике же у всех переменных статически один тип — any/dynamic.
В языке по ссылке при отсутствии определённых конструкций типа все типы выведутся и всё будет статическим. Какой же он динамический-то?
Посмотрите, какой тип он выводит так такой штуки — функции, проверяющей, что поданная на вход функция (с любым кол-вом аргументов) всегда вернёт true на любом входе.
Если упростить тип для понимания, то он такой:
Кстати, немного оффтоп, есть такой канонический пример нетипизируемого лямбда-выражения:
В Agda, например, его можно типизировать:
Если «построить отдельный рантайм» с нужными свойствами, получится язык со статической или динамической типизацией?
Да, но обобщить несложно, не так ли?
Тип
Dynamicи в Хаскеле есть, к примеру. Другое дело, что там им неудобно пользоваться, но это уже ортогональный вопрос.Вот посмотрите также на Soft types для ML-like языка.
Совсем вкратце про soft types: добавляются дополнительные правила вывода. В некоторых конкретных случаях при ошибке вывода выводится dynamic/any. Typescript, собственно, вроде как раз soft types и есть, просто он совместим с JavaScript, что накладывает ограничения. В статье приводится ML-like статический язык с такими же особенностями.
Например, для положительного числа x, пришедшего по сети, число x*2 + 1 всё равно больше, чем x, и такую пару можно передать без проверок.
Если же про оба числа ничего неизвестно, то, понятно, надо сделать динамическую проверку руками до вызова функции. Например, так:
if x < y then ... тут x < y, можно звать функцию ... else ... а тут нет ...
см Изоморфизм Карри — Ховарда
Ну на самом деле проблема несколько в другом. Я, например, смогу объяснить, но это требует усилий, чтобы пользоваться не привычным понятийным аппаратом, а тем, который понятен собеседнику. Ему действительно настолько интересно, что трата моих ресурсов на объяснение будет оправдана? Нередко ведь спрашивают «так, разговор поддержать».
С этим абсолютно не согласен. Зачем рассказывать о том, чем занимаешься? Мне достаточно того, что мне нравится, чем я занимаюсь.
PS> function ap($a) { & (gcm -c ap $a) $args }
PS> ap curl
...
PS> ap curl --help
...
P.S. Ага, увидел в ссылке на github ваш вариант, с '^'
Он и короче, и функциональнее.
Что-то я ничего не могу нагуглить, а эксперименты в ps не помогают понять
Заканчивайте в любой удобный момент.
А правильно — это как? Так, чтобы работала? Ну тогда любая команда работает, если её правильно написать, но это уже какое-то альтернативное толкование слов.
По-моему, это вы так и не заметили, что с Krey вы обсуждали именно то, о чём пишу я, от этого у вас такое недопонимание сначала его, а потом и меня. Не верите, спросите его лично, он вам подтвердит. Или хотя бы обратите внимание на его ответ мне, где он подтверждает мои слова.
Команда работает, будучи другой командой.
Я вам помогу. Ветка началась с этих сообщений:
Во всей ветке речь идёт именно о том, что не работает команда, а не программа. И под не работает подразумевается именно что, что это и значит — не делает то, что задумано. Я вам даже процитирую, что было задумано:
А теперь будьте добры, покажите, где шла речь о том, что не работает программа find.
Неработающая команда, это вот эта, привожу её ещё раз целиком:
Не утилита find нерабочая, а вся целиком эта команда (find — не команда), так как она не делает то, что просили. Работоспособность и корректность самого find никто не оспаривал.