Еще inline-java есть у нас

Пока только байндинги правда, без TH

http://www.mathstat.dal.ca/~selinger/quipper/

Вдохновлялись хаскелем видимо

Только где достать квантовый компьютер??

Вдохновлялись хаскелем видимо

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

Только где достать квантовый компьютер??

Квантовый компьютер доставать не нужно, его нужно эмулировать.

Видел где-нибудь симулятор для по играться?

Видел где-нибудь симулятор для по играться?

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

Прикольно, многие реально пытаются симулировать квантовые процессы

Ребята сможет понятно объяснить что такое "type level" программирование - так то я интуитивно понимаю -> хочется чёткого определения?

это кодирование инвариантов программы при помощи типов

те это только подходит для яп с сильными типами?со слабыми типами это невозможно?

Для начала надо определиться, о чем речь. Если ты в с++ явно опрделяешь тип переменной, то это уже кодирование инварианта, и можно рассматривать как простиейший вид type level coding. В хаскеле можно кодировать инварианты с более сложными условиями.

Ну например джаваскрипт - слабая типизация - т.е. тайп левел программирование там невозможен ( инвариантность бесконечна - даже если неправильное выражение - всё равно отработает , а что будет в результате хз), а на хаске сильная - там это сам бог требует т.е. это возможно (может я неправильно сформулировал вопрос?)

это кодирование инвариантов программы при помощи типов

Кстати это определение мне нравится(надо записать)?

На размышления меня подвинула статья https://habrahabr.ru/post/308484/

Особенно про Idris - он же ссужает диапазон возможных ошибок -> и снижает затраты и время на тестирование(имхо)

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

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

Да но я имел ввиду статическую - но сильную и слабую , например Haskell vs Golang

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

И тут хаск - но вот сможет кто нибудь кинуть мне ссылку - на премущества ленивости vs жадности)

https://ru.wikipedia.org/wiki/%D0%A1%D0%B8%D0%BB%D1%8C%D0%BD%D0%B0%D1%8F_%D0%B8_%D1%81%D0%BB%D0%B0%D0%B1%D0%B0%D1%8F_%D1%82%D0%B8%D0%BF%D0%B8%D0%B7%D0%B0%D1%86%D0%B8%D1%8F судя по определению сильная типизация это та, которая позволяет больше возможностей для типизации.

Да сиогласен - но вот для меня яркими антиподами для статических типов - Хаскель и Голанг

голанг.....

я так много слышу о нем в последнее время

У него логтип клевый

это привлекает людей

маркетинг

Голанг тестить надо хорошо - сам столкнулся type ( user struct { ID int json:"id" Name string json:"name" Age int jsom:"age" } )

Скомпилась без вопросов - только молча json поле age было Age - c заглавной

а другие с прописной?

А я думал что это элм противится)

а другие с прописной?

да посмотри - там опечатка в поле age

А я думал что это элм противится)

Вообще с этим бида Поэтому для Go есть масса санитайзеров

> jsom да, смешно

я так понял, json тут - аннотация, которая используется библиотекой для генерации json и эта библиотека молча использует имя поля, если не нашла нужную аннотацию

я так понял, json тут - аннотация, которая используется библиотекой для генерации json и эта библиотека молча использует имя поля, если не нашла нужную аннотацию

Так и есть

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

Вот фронт на елме

Вот фронт на елме

о

эльммен

на эльме можно как на джс?

Превалидация

(я всмысле что-то серьезное)

Какой-то бред, если честно. Простите, если кого обидел.

или еще сыроват?

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

Он этим и прекрасен Люди устали от теории категорий и хотят байтоебства

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

на эльме можно как на джс?

Да там прямо интерактивно всё делать можно (без всяких выкрутасов) - а типы строго проверяет

Динамическая, статическая, сильная, слабая типизация... Пофиг. Это можно парадигмой назвать. Или шаблоном. Как процедурное программирование.

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

чем это лучше определения выше?

Динамическая, статическая, сильная, слабая типизация... Пофиг. Это можно парадигмой назвать. Или шаблоном. Как процедурное программирование.

Всё таки я вангую что со повышением сложности сильно типизированные ЯП выиграют - но ленивость убъёт многих))))

Всё таки я вангую что со повышением сложности сильно типизированные ЯП выиграют - но ленивость убъёт многих))))

Время покажет

чем это лучше определения выше?

Потому что слово "инварианты" знакомо примерно 5% людей и еще меньше людей правильно его понимают.

на эльме можно как на джс?

А мне отладчик - пока костыль понравился ( говорят будет более лучше - пробы с версиями ) - Время неимеет значение - важна жизнь(с) (5й элемент)

Главное, что понимают его меньше людей, чем используют.

Потому что слово "инварианты" знакомо примерно 5% людей и еще меньше людей правильно его понимают.

можно тест? неизменные сущности?

Если кому интересно могу кинуть исходник быдло кода н аэлме)))

можно тест? неизменные сущности?

В чем смысл "теста"? Хочешь, чтобы я подтвердил или опроверг, что ты входишь в те <5%?

да

ERROR: S client not available

можно и так

да

Ок, ты точно попал в 5% Для остального слишком мало написал. У слова слишком много вариантов использования.

ееееееее

ееееееее

Тут видишь какое дело. Так и не стало понятно, как эти "неизменные сущности" применить к программированию, основанному на типизации.

Тут видишь какое дело. Так и не стало понятно, как эти "неизменные сущности" применить к программированию, основанному на типизации.

да

2 тест : объекты должны иметь инвариантный тип?

(хотя если чесно херню сморозил ибо по смыслу "исключить полиморфное поведение")

https://ru.wikipedia.org/wiki/%D0%A1%D0%B8%D0%BB%D1%8C%D0%BD%D0%B0%D1%8F_%D0%B8_%D1%81%D0%BB%D0%B0%D0%B1%D0%B0%D1%8F_%D1%82%D0%B8%D0%BF%D0%B8%D0%B7%D0%B0%D1%86%D0%B8%D1%8F судя по определению сильная типизация это та, которая позволяет больше возможностей для типизации.

Для меня сильная типизация - это отсутствие неявного приведения типов Всё

это как раз слабая

Хитрый ход :)

это как раз слабая

То есть в js сильная типизация?

Но нет, сильная и слабая типизация это не черное и белое. Там посередине дофига оттенков

Да я согласен - термин чётко пока не сформулирован

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

Например, один язык позволяет прибавить к строке число, а в другом есть конструктор даты из строки. В каком из них типизация сильнее или слабее?

это вообще не говорит о типизации

Или вот, если в языке к строке можно символ добавить, это делает типизацию слабой?

Да конструкторы это не типы - их можно реализовать как хочешь

Или вот, если в языке к строке можно символ добавить, это делает типизацию слабой?

Ты про String + char?

Например, один язык позволяет прибавить к строке число, а в другом есть конструктор даты из строки. В каком из них типизация сильнее или слабее?

Смотря как и где программист указывает тип

Ты про String + char?

Да

Да конструкторы это не типы - их можно реализовать как хочешь

Ну, ок, ок, плохой пример

В смысле, если внешне конкатенация двух строк и прибавление числа к строке неотличимы и это валидная операция - то это слабая типизация

Хотя это всё вопрос терминологии

Я думаю что вкладывают в понятие например String и в Char создателя языка

Да уж, ребятки. Вот есть у нас "замечательный" язык C++, прости господи. В нем нельзя сложить строку и символ. Но я могу перегрузить оператор сложения и определить нужную операцию. И, о чудо, строка начала складываться с символом!

Товарищи, есть пакеты Text.Parsec и Text.ParsecCombinators.Parsec

и у них некоторые функции пересекаются

кто-то обьяснит почему так?:)

кто-то обьяснит почему так?:)

Интересный вопрос :)

Re: type level programming