Кстати по-этому вам следовало бы подправить ваше определение «не строгой» типизации, и указать, что в описываемом языке у функций не указываются типы параметров (это НЕ-«третий пункт с вики») и что значения могут неявно преобразовываться, например, с числа в строку (это НЕ-«четвертый пункт с вики»).
Я понял. Проблема не в вас, проблема в википедии.
Первых два пункта не относятся к строгой типизации.
Что интересно, там ниже указан Питон, для которого кстати эти два первых пункта и не выполняются — противоречие блин.
Короче нужно осторожней с википедией=)
> Это значит, что в момент объявления переменной мы не обязаны указать какого она типа, и более того во время работы программы в эту переменную можно ложить данные абсолютного любого типа.
> приём, широко используемый в языках программирования и языках спецификации, при котором переменная связывается с типом в момент присваивания значения, а не в момент объявления переменной. Таким образом, в различных участках программы одна и та же переменная может принимать значения разных типов. Примеры языков, где есть динамическая типизация — Smalltalk, Python, Objective-C, C#, Ruby, PHP, Perl, JavaScript, Lisp, xBase.
Ваше предложение со статьи и комментарий с википедии говорят о тех же вещах.
Но на википедии говориться о динамической типизации, вы же это приписываете не строгой типизации — а это ортогональные свойства.
>… не строго типизированный язык. Это значит, что в момент объявления переменной мы не обязаны указать какого она типа, и более того во время работы программы в эту переменную можно ложить данные абсолютного любого типа.
Это свойство «не статической типизации».
Вот например Питону описанное тоже присуще, но он строго типизированный.
А С++ не присуще, но он НЕ строго типизированный.
*(Но нужно понимать, что в статье вы построили модель мира (ну точнее взяли существующую систему), а одной из основных характеристик модели есть адекватность, и только когда модель достаточно адекватна, результаты полученные с ее помощью можно применять к моделируемой системе)
Да, эта тема тоже весьма интересная, я планирую позже ею тоже заняться.
Основой для верификации команд ассемблера ведь есть аксиомы, что те или иные команды имеют некоторый тип?
Если это так, то доказательство правильности программ можно доказывать и с помощью Агда (хотя наверное это немного не то).
*буду иметь Вас ввиду:)
Имел (имею?) дело с эзотерикой в программировании.
Спасибо.
Первых два пункта не относятся к строгой типизации.
Что интересно, там ниже указан Питон, для которого кстати эти два первых пункта и не выполняются — противоречие блин.
Короче нужно осторожней с википедией=)
> Это значит, что в момент объявления переменной мы не обязаны указать какого она типа, и более того во время работы программы в эту переменную можно ложить данные абсолютного любого типа.
> приём, широко используемый в языках программирования и языках спецификации, при котором переменная связывается с типом в момент присваивания значения, а не в момент объявления переменной. Таким образом, в различных участках программы одна и та же переменная может принимать значения разных типов. Примеры языков, где есть динамическая типизация — Smalltalk, Python, Objective-C, C#, Ruby, PHP, Perl, JavaScript, Lisp, xBase.
Ваше предложение со статьи и комментарий с википедии говорят о тех же вещах.
Но на википедии говориться о динамической типизации, вы же это приписываете не строгой типизации — а это ортогональные свойства.
Да, я вместо «динамическая типизация» написал «не статическая типизация», вы на это намекаете?
Это свойство «не статической типизации».
Вот например Питону описанное тоже присуще, но он строго типизированный.
А С++ не присуще, но он НЕ строго типизированный.
*(Но нужно понимать, что в статье вы построили модель мира (ну точнее взяли существующую систему), а одной из основных характеристик модели есть адекватность, и только когда модель достаточно адекватна, результаты полученные с ее помощью можно применять к моделируемой системе)
Основой для верификации команд ассемблера ведь есть аксиомы, что те или иные команды имеют некоторый тип?
Если это так, то доказательство правильности программ можно доказывать и с помощью Агда (хотя наверное это немного не то).
*буду иметь Вас ввиду:)
Может вам интересно будет — он С-ориентирован.
Виват Функциональное!
Виват Бесточечное!
*(еще вот такое есть — похоже на ваше)