Человеческое метапрограммирование

Собственно это ключевой момент. _любое_ значение _всегда_ содержит полную информацию о своем типе в рантайме. Потому что тип значения - это любое множество, которому это значение принадлежит.

а какому множеству принадлежит значение 0x40400000 ? ну или даже проще — это (float)3 или (unsigned int)0x40400000 ?

Сорри, это пример в статье «Languages as Libraries»

Ну там просто проверка на лямбду, хз

Схематичный тайпчекер для Typed Racket, приведенный в этой статье, работает так же. И сказано «while this module-level typechecker is simple, the full implementation for Typed Racket employs the same strategy», так что схематичность не играет роли.

http://repository.readscheme.org/ftp/papers/sw2007/01-culpepper.pdf

На первый вгляд - то же, что и «Languages as Libraries».

Typed Scheme installs a #%module-begin macro that first per- forms the normal module expansion (using local-expand), analyzes the result, and produces a module body that follows a new module variable protocol that provides the type-checker with the types of module variables:

(define-syntax (module-begin stx)
 (syntax-case stx ()
   [(module-begin form . . . )
    (type-check-module-body
      (local-expand #’(#%plain-module-begin form . . . )
                   ’module-begin
                   null))]))

Т.е. тайпчек выполняется во время расширения макроса module-begin, и сообщения об ошибках наверняка относятся к расширенному коду.

_любое_ значение _всегда_ содержит полную информацию о своем типе в рантайме

или вот так — что больше, 0x70000000 или 0x90000000 ? при этом известно, что эти 4 байта представляют собой неразмеченный

union { int sig_int; unsigned int unsig_int; }

Мне надо знать что в точке вызова yoba тип будет t243, тайпчекер мне это _статически_ гарантирует, что еще?

x = read ....

if (x > 42)
    print x ...

^ мне тайпчекер «статически» гарантирует, что в точке вызова print - x > 42. Это то же самое - какое-то очень специфическое представление о статических гарантиях.

У меня в примере были сложные структуры? нет, не было.

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

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

enum tag { INT, STRING };
struct obj { enum tag tag; };
struct int_obj { enum tag tag; int value; };
struct string_obj { enum tag tag; char *value; };

void dyn_print(struct obj *obj)
{
    switch (obj->tag) {
        case INT: printf("%d\n", ((struct int_obj*)obj)->value); break;
        case STRING: printf("%s\n", ((struct string_obj*)obj)->value); break;
    }
}

    struct int_obj i = { .tag = INT, .value = 42 };
    dyn_print((struct obj*)&i);

или тегированными указателями (как в SBCL/Factor), то это другое дело:

union int_string_obj { struct int_obj i; struct string_obj s; };

    union int_string_obj is;

    if (getchar() == '0') {
        struct int_obj i = { .tag = INT, .value = 42 };
        is.i = i;
    } else {
        struct string_obj s = { .tag = STRING, .value = "24" };
        is.s = s;
    }

    switch (is.i.tag) {
        case INT: printf("%d\n", is.i.value); break;
        case STRING: printf("%s\n", is.s.value); break;
    }

Но оно работает без динамических проверок и тайптегов.

Выше ты уже сказал

Ну да он отрабатывает в рантайме.

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

Вместо when будет if - если ты не хочешь называть это динамической проверкой, а хочешь верить, что тайпчекер умеет телепатию, то ладно. Числа, разумеется, не будут тегироваться (но на практике нормальный анбоксинг мало где есть).

есть еще как минимум один случай

Это не шаблонный union?

а какому множеству принадлежит значение 0x40400000 ?

К любому множеству, содержащему это значение. Что за глупый вопрос? Например к множеству, в которое только это значение и входит. Или к множеству, в которое входит это значение и еще какое-нибудь. или к множеству в которое входит это значение и любой другой набор любых других значений.

^ мне тайпчекер «статически» гарантирует, что в точке вызова print - x > 42. Это то же самое - какое-то очень специфическое представление о статических гарантиях.

В данном случае тайпчекер статически ничего не гарантирует. Т.к. если print будет иметь тип print: (> 42) -> Void, то тайпчекер такую конструкцию пропустит. У меня же тайпчекер _в компайлтайме_ проверяет, что в точке вызова yoba х обязана иметь тип t243. Если вдруг окажется что она там может иметь другой тип - будет ошибка (в компайлтайме). Рассуждая как ты - статических гарантий вообще ни в каких ЯП не бывает.

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

Давай по порядку. Сперва закончим с моим примером. Итак:

1. в моем примере ничего не боксится и никаких тегов нет.

2. в моем примере чекер статически гарантирует что в точке вызова yoba тип х будет t243 (статически - значит он выводит тот факт в компайлтайме и там же в компайлтайме кидает ошибку, если факт не может быть выведен).

что здесь тебе непонятно?

Выше ты уже сказал

Ну да, when отрабатывает в рантайме. по-этому в компалтайме чекер гарантирует, что внутри yoba нужный тип.

Вместо when будет if - если ты не хочешь называть это динамической проверкой, а хочешь верить, что тайпчекер умеет телепатию, то ладно.

При чем тут телепатия? Тебе нужна телепатия, чтобы посмотрев на программу (when (= x 243) ...) сказать, не выполняя ее, что на месте многоточия переменная х обязательно будет иметь значение 243?

ну по такой логике любой тайпчекер в любом языке занимается телепатией :)

например хаскель, определим ф-ю f x = x + 1. Тебе тайпчекер гарантирует, что никто в рантайме не вызывает эту ф-ю с аргументом строкой. Это телепатия, да?:)

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

или вот так — что больше, 0x70000000 или 0x90000000 ?

Что значит «больше»? Не понимаю вопроса :(

при этом известно, что эти 4 байта представляют собой неразмеченный

Какая разница что они представляют? Забудь, эта информация бесполезна и ни на что не влияет. У тебя есть два байта - все. Это первично. Система типов должна моделировать возможности различать эти байты - и более ничего, это ее цель. Примитивные системы типов просто делают это плохо, в итоге появляются какие-то «представления» и прочая чушь - вплоть до того, что типы могут быть у термов (это как же надо оболбаться, чтобы такую хуйню на полном серьезе рассматривать?!) или одно и то же значение может иметь разный тип, в зависимости от того в каком терме оно появляется, причем один тип не является подтипом другого! Бред полный.

В данном случае тайпчекер статически ничего не гарантирует

Тогда так:

#include <stdio.h>
#include <stdbool.h>

struct A { char value; };
struct B { char value; };
struct A _a = { .value = 'a' };
struct B _b = { .value = 'b' };
union AB { struct A a; struct B b; };
struct A sup(union AB x) { return x.a /* == x.b */ ; }
bool a_pred(union AB x) { return sup(x).value == 'a'; }
bool b_pred(union AB x) { return sup(x).value == 'b'; }
struct B fun(struct A a) { return _b; }

int main()
{
    union AB x;
    if (getchar() == '0') x.a = _a; else x.b = _b;
    if (a_pred(x)) printf("%c\n", fun(sup(x)).value);  // (1)
    if (b_pred(x)) printf("%c\n", fun(sup(x)).value);  // (2)
    if (!b_pred(x)) printf("%c\n", fun(sup(x)).value); // (3)
    if (!a_pred(x)) printf("%c\n", fun(sup(x)).value); // (4)
}

то есть суть в том, что чекер пропустит (1) и (3), но не пропустит (2) и (4)?

в моем примере ничего не боксится и никаких тегов нет.

Допустим, это вырожденный случай - в си юнион объектов одного типа с одинаковым memory layout не нужен. Теперь представим, что A и B существенно отличаются - чтобы написать те предикаты нужно добавить теги либо им, либо юниону.

то есть суть в том, что чекер пропустит (1) и (3), но не пропустит (2) и (4)?

Да. Я же приводил тот же самый пример и там писал что будет пропущено, а что - нет. И само по себе «printf(»%c\n", fun(sup(x)).value);" (то есть не внутри if-ветки) тоже пропущено не будет чекером.

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

Ты опять не можешь отойти от дедовских типов. Первичны значения, у значений есть типы. Типы не бывают без значений. Если два значения нельзя различить - они имеют одинаковый тип. По определению. Если нам, например, надо, чтобы вот тут 0 воспринималось как булево значение, а в другом месте тот же 0 воспринимался как число, и тайпчекер не пропустил «смешивание» этих типов, то нам надо самим сконструировать различимые значения, например (cons 'bool 0) и (cons 'int 0). И писать соответствующий код. И тайпчекер тогда гарантирует что в том месте где должен быть Bool у нас будет именно (cons 'bool 0), а не (cons 'int 0). Другими словами эти теги не будут встроены в семантику ЯП и семнатику тайпчекера, мы их реализовываем сами тем или иными способом, или не теги а какой-то альтернативный механизм, а чекер гарантирует нам, что все хорошо. И, естественно, мы сами сможем вот так вот боксить/анбоксить значения как нам угодно.

анонимус, а что ты думаешь про выразительность системы типов Qi?

У него проблемы с корректностью, то есть через его sequent calculus можно заставить чекер вывести ошибочный тип.

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

1. чтобы данный терм принимал указанное множество значений

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

Второй пункт выражается через первый (путем ручного боксинга/анбоксинга). Недостаток у него один - производительность, повышенные потребности к памяти. Решения есть два:

1. реализовать параллельную систему, которая будет давать именно гарантии второго типа

2. Хороший оптимизатор.

У первого пути есть некоторые преимущества - оно по производительности все ранво будет лучше оптимизатора и «искаробки» дает некоторое количество синтаксического сахара.

Ты опять не можешь отойти от дедовских типов

При чём тут какие-то дедовские типы (второй раз уже советуешь мне от чего-то зачем-то отказаться)? У типов есть значения (лучше, если всегда более нуля), у значений есть типы (начиная с минимального). Я всегда предпочту какую-то определённую наперёд индуктивную систему формирования значений и типов туманному подходу «любое значение может иметь любой тип». Можно начать с типов - обзывать их по порядку просто как объекты универсума (и, с другой стороны, как подкатегории, функторы из терминальной категории в универсум или эндофункторы на универсуме), потом обзывать конструкторы термов как стрелки с правилом композиции из разных типов в определяемый, образуя граф подкатегории, и функции как такие же стрелки с правилами переписывания одних термов в другие.

Если два значения нельзя различить - они имеют одинаковый тип.

Есть разные выражения составленные по определённым правилам и приобретающие определённые типы (тоже по правилам). Часто, в большинстве языков, то какие выражения приобретают какой тип захардкожено синтаксически (для примитивных типов). Для всего остального есть принятая в языке система образования множеств значений заданных пользователем языка типов (конструкторы типов, конструкторы значений, геттеры с сеттерами).

Я всегда предпочту какую-то определённую наперёд индуктивную систему формирования значений и типов туманному подходу «любое значение может иметь любой тип».

Почему же любой? Оно может иметь только тот тип, элементом которого является.

А эти «индуктивные системы» - как раз и есть пережиток прошлого. Они нужны только из-за неразвитости средств. Система типов не имеет никакой ценности сама по себе, она не первична. У нас есь задача и система типов должна ее решать. Сейчас же все происходит с точностью до наоборот - боженька теоретикам дает систему типов, а какое отношение она имее к реальности - ну это не важно.

Можно начать с типов - обзывать их по порядку просто как объекты универсума

Типы - это не объекты универсума, точнее не любые объекты не любого универсума. По определению, тип - это множество значений. Все. Все остальное (с объектами универсума, стрелками, категориями и прочей ненужной чепухой) - это устаревшие теории для бедных. Что называется «на безрыбье и рак рыба» - то есть если с корректной системой типов работать возможности нет, то приходится строить заведомо некорректную модель на категориях, стрелках, функторах. Она, конечно некорреткна - но как-то (с пятого на десятое) работает.

Есть разные выражения составленные по определённым правилам и приобретающие определённые типы (тоже по правилам).

У выражения _нету типа_. Это - ересь, забудь про эту ересь. Тип есть у значений и только у них. Ты привык к тому, что тип - это какая-то НЕХ, которую мы по определенным правилам приписываем термам, так вот нет - это лишь примитивная модель. У нас есть ЯП, в этом ЯП есть значения. Любе подмножество этих значений - есть тип. Можно _условиться_ называть типом терма тип значений, которые он может принимать. Мы не приписываем термам типы. Типы термам дает боженька и control-flow - то есть если согласно control-flow программы терм может принимать такие-то значения - такой у него и тип. Другими словами, тип терма - экспериментальный факт. Это то, что мы наблюдаем (и никак не можем определить иначе чем путем наблюдения) и можем пощупать (никакие другие типы нам не нужны - другие типы нам решать задачу не помогут). Именно это (эксперимент и наблюдение) лежит вначале. Правила вывода - не лежат вначале. Правила вывода - это лишь некая попытка на основе анализа кода программы предсказать какие типы будут у термов в рантайме (до рантайма никаких типов нет, т.к. значений нет, а типы, см. выше, существуют только у значений). Правила типизации - это лишь некая модель. Если эта модель реальности соответствует (то есть позволяет точно расчитать типы, которые будут согласовываться с результатами наблюдений) - это хорошая, годная модель. Если не позволяет - выкинуть на помойку эту хуйню. Не путай реальность и модель.

Я всегда предпочту

То есть ты не можешь ничего предпочесть. Система типов тебе _дана_ и она _зафиксирована_. Все что ты можешь - выбрать модель по-лучше.

Дяди, можно я вмешаюсь в вашу высокоинтеллектуальную дискуссию?

У выражения _нету типа_. Это - ересь, забудь про эту ересь. Тип есть у значений и только у них.

А если выражения могут быть значениями?

А если выражения могут быть значениями?

Ну конечно у него может быть тип как у значения. Но у (+ 1 2) будет тип далеко не Int, ясное дело.

Эм... А какой? Int × Int → Int это у +. Значит у (+ 1 2) по идее что-то вроде (Int × Int → Int) × Int × Int → (?) Int?

Эм... А какой?

Expr ... - ну а что там вместо многоточия не суть важно.

Expr ...

У этого треда уже своя мифология? И типы Expr ... у 1 + 2...

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

У этого треда уже своя мифология? И типы Expr ... у 1 + 2...

Ну у 1 + 2, а у [| 1 + 2 |].

Это же при латентной типизации принято отказываться от типов выражений

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

Эм... И как модель «Expr ...» позволит проверить правильность типов до рантайма? Я не думаю, что есть хоть какой-то смысл в модели, которая может сказать только «это выражение».

Эм... И как модель «Expr ...» позволит проверить правильность типов до рантайма? Я не думаю, что есть хоть какой-то смысл в модели, которая может сказать только «это выражение».

Expr - это у [| 1 + 2 |], у 1 + 2 будет тип 3 < Integer.

Ну у 1 + 2, а у [| 1 + 2 |].

Ок, тип 1 + 2 совпадает с типом нормальной формы 3 - будет int в си, то что в default Num в хаскеле и т.п. У квазицитаты тип Expr Int. Кстати, в хаскеле как раз нет проблем в том чтобы 0, 1 и т.п. подобные числовые литералы трактовались как Bool, Int, Integer и что угодно, так же как нет проблем в том чтобы литералы строк трактовались как String, ByteString, Text, JSON или что угодно, в зависимости от ситуации.

в хаскеле как раз нет проблем в том чтобы 0, 1 и т.п. подобные числовые литералы трактовались как Bool, Int, Integer и что угодно, так же как нет проблем в том чтобы литералы строк трактовались как String, ByteString, Text, JSON или что угодно, в зависимости от ситуации.

Ну это просто слабая типизация. Вон в сишке еще хлеще. Была бы сильной (как в нормлаьных языках) - нельзя бало бы так делать.

Ну это просто слабая типизация. Вон в сишке еще хлеще. Была бы сильной (как в нормлаьных языках) - нельзя бало бы так делать.

А я думал, что слабая типизация — это возможность трактовать значение как значение ортогонального типа (Int как String), а не как значение над-/подтипа. Типа: строковой литерал «1» имеет собственный, наиболее глубокий в иерархии тип NumberString, и его можно свободно трактовать (приводить) к типам FloatString, String, Text и т. п., но никогда к Float, или там JSON_String.

Хотя, к FloatString по идее нельзя. Только вверх к более общим типам. «1» катит только как общий NumberString, потому что FloatString, IntegerString ⊂ NumberString, но FloatString ⋂ IntegerString ≠ ∅

Ну это просто слабая типизация.

Там перегрузка литералов, типизация строгая. Строки это всё что IsString, например:

{-# LANGUAGE OverloadedStrings #-}

import Data.Aeson
import Data.String
import Data.Maybe
import Control.Applicative

stringAsString :: String
stringAsString = "string"

data Data = Data { integer :: Integer, string :: String }
  deriving ( Eq, Show )

instance FromJSON Data where
  parseJSON (Object v) = Data <$> v .: "integer" <*> v .: "string"

instance IsString Data where
  fromString = fromJust . decode . fromString

dataAsString :: Data
dataAsString = "{ \"integer\" : 5, \"string\" : \"string\"}"
-- ^ Data {integer = 5, string = "string"} == dataAsString => True

а числа - всё что Num:

instance Num Bool where
  (+) = (||)
  (*) = (&&)
  abs = id
  signum = id
  fromInteger 0 = False
  fromInteger 1 = True

intAsNumber :: Int
intAsNumber = 5

boolAsNumber :: Bool
boolAsNumber = 1
-- ^ boolAsNumber == True => True

(оба примера предполагают возникновение исключений).

В статике выражения _имеют_ тип, парсер разбирает число как Integer, строку как String, если дальше видно что выражения имеют другие типы X и Y, соответственно, то ищутся специализации fromInteger :: Integer -> X и fromString :: String -> Y для типов X и Y, то есть инстансы Num и IsString. Всё это происходит во время компиляции. Правда, fromInteger и fromString работают в рантайме, что уже не так хорошо.

А я думал, что слабая типизация — это возможность трактовать значение как значение ортогонального типа (Int как String), а не как значение над-/подтипа.

Именно так. В хаскеле над/подтипов нет, по-этому любые два типы ортогональны.

Строки это всё что IsString, например:
а числа - всё что Num:

Так ни то ни другое не является типами. Это все тайпклассы. Тип - это допустим Data в твоем примере. Или Integer. Или String. Или Bool.

В статике выражения _имеют_ тип

Еще раз, ТЕРМЫ НЕ ИМЕЮТ ТИПОВ. Нигде. Запомни. Это аксиома. Если ты не поймешь таких базовых вещей, до идти дальше смысла просто нет.

Типы есть у _значений_. И только у них. И они ДАНЫ. Их нельзя выбирать. Тогда можно определить тип терма, как тип возможных значений терма. И эти типы тоже ДАНЫ. Они не зависят от каки-то там правил типизации языка и прочих бредней - они определяются из экспериментальных наблюдений. А правила типизации следует выбирать так, чтобы они наблюдениям не противоречили. Любая модель в которой у терма есть несколько типов не будет корректной, т.к. противоречит практическим результатам. А значит смысла в этой модели нету никакого.

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

анонимус, тебя на поворотах заносит, и ооооочень далеко (хотя для дискуссии это и интересно)

понятно, что статические типы

1) являются аппроксимацией инвариантов рантайма

2) исторически стремятся ко все более точной аппроксимации

3) исторически отходят от syntax-driven вычислимости,

и поэтому типом разумно называть любой инвариант рантайма (осторожно: подобные заявляения могут вызвать мощный баттхерт у хаскелистов)

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

или вот так — что больше, 0x70000000 или 0x90000000 ?

Что значит «больше»? Не понимаю вопроса :(

ну вот, ты не знаешь, как применить к этим бинарным данным определенную функцию; это намек тебе, что определение типа как множества несовершенно — ты должен был сказать что-то про операции

при этом известно, что эти 4 байта представляют собой неразмеченный

Какая разница что они представляют? Забудь, эта информация бесполезна и ни на что не влияет. У тебя есть два байта - все. Это первично.

байты важны, но не первичны; важно именно что, что эти байты представляют

Система типов должна моделировать возможности различать эти байты - и более ничего, это ее цель.

на всякий случай замечу, что типы могут быть не только у значений (это функционалистский взгляд) но и у переменных, которые конкретными байтами сейчас не являются; да и еще значение может быть optimized out, и опять байтами не являться

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

void print1() { putchar( 0x31 ); } // значение '1' в ascii и юникоде
register int x = ... ;
if(x==1 /* сразу после сравнения регистр, где лежал х, можно затереть */) {
   print(x) ; // может быть оптимизированно до print1();
} //     ^ вот это х по твоему что, не значение? но бинарно его нигде нет

Примитивные системы типов просто делают это плохо, в итоге появляются какие-то «представления» и прочая чушь - вплоть до того, что типы могут быть у термов (это как же надо оболбаться, чтобы такую хуйню на полном серьезе рассматривать?!)

да, типы могут быть у термов, *например*, после того, как известны типы составных частей термов

скажем, у терма x+y может быть тип int, если известно, что такой тип имели x, y, и оператор + этот тип сохраняет,

а так же у него может быть тип вот уж не знаю что, но что-то большее (полиморфного) нуля из некого множетсва с коммутативной операцией «+» и с порядком «>», согласованным c операцией «+», если такой тип имели x, y

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

конечно может

скажем, значение 0 может иметь 2 типа неотрицательное_целое и неположительное_целое; при этом, оно будет иметь эти разные типы, в зависимости от терма — а еще точнее, от контекста, где мы, скажем, накапливаем в некоторую переменную сумму соответствующего знака

Это не шаблонный union?

не понял вопрос и не понял, к чему он

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

типа вот это template<class T> union U { ...... } просто назвать типом U?

нет, я предполагаю пример в виде union U { A a; B b; }

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

ну да, даже с твоим подходом «типы это множества» число 0 имеет как минимум 2 типа {0, 1} и {0, 2}, причем ни один тип не является подтипом другого

и кто тут бредит?

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

Я понимаю, но заебывает, когда на все один ответ: «А вот у меня в хаскеле нитак, значит это неправильно!1!1!!» (не, ну реально, до чего дошло - товарищ аргументирует невозможность существования корректных систем типов в которых будут типы для отдельных значений, тем, что это В АГДЕ НЕ ВЫРАЖАЕТСЯ!). Так что я решил отвечать такой же ебнутой упертостью.

ну да, даже с твоим подходом «типы это множества» число 0 имеет как минимум 2 типа {0, 1} и {0, 2}, причем ни один тип не является подтипом другого

Ну да, уел :)

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

ну вот, ты не знаешь, как применить к этим бинарным данным определенную функцию; это намек тебе, что определение типа как множества несовершенно — ты должен был сказать что-то про операции

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

скажем, у терма x+y может быть тип int, если известно, что такой тип имели x, y, и оператор + этот тип сохраняет,

Ну это уже наша модель.

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

1. Значение принадлежит определенному множеству.

2. К значению на данном control-flow не применяется операций, не принадлежащих данному интерфейсу.

3. Какие еще?

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

Т.е. тайпчек выполняется во время расширения макроса module-begin, и сообщения об ошибках наверняка относятся к расширенному коду.

Ну да, то есть тайпчек происходит после экспанда. А тебе что нужно было?

то есть тайпчек происходит после экспанда. А тебе что нужно было?

Хотел спросить, является ли это АДОМ И ПОГИБЕЛЬЮ в практике работы с Typed Racket.

не понял вопрос и не понял, к чему он

На С++ можно извратиться - сделать список параметризованный своей длинной в шаблоне и сделать безопасную индексацию с контролем выхода за границы в compile-time. Могу предполагать, что также можно сделать union параметризованный номером поля и сделать безопасные геттер/сеттер с контролем за тем, что доступ будет происходить ровно к тому полю которое было инициализировано при создании/изменении объекта этого union. Тоже в compile-time. Но этим всё равно невозможно будет пользоваться.

я предполагаю пример в виде union U { A a; B b; }

Тогда без понятия. Если A == B, если A и B сами тегированы (как-то узнаваемы в рантайме), либо если обернуть U в структуру с тегом - больше ничего не приходит на ум.

Тип - это допустим Data в твоем примере

И там сделано так, что строки можно использовать на тех местах где ожидается Data, потому что определено соответствующее преобразование String -> Data (инстанс класса IsString, да). По сути, любая «строка» это (fromString «строка»), а любое число - (fromInteger число), для String и Integer обе функции = id, для всего остального можно придумывать произвольные преобразования.

Еще раз, ТЕРМЫ НЕ ИМЕЮТ ТИПОВ. Нигде. Запомни. Это аксиома.

Хочешь сказать, что в модельной категории у стрелок нет объектов? Или что в модельных системах типов из TAPL/ATTAPL/whatever все правила формирования _типов_ для сложных _выражений_ это ни о чём? Смотри:

Bool : U(0)
true : Bool
false : Bool

p : Bool, x : T, y : T
----------------------
if p then x else y : T

или

Bool : 1 -> U(0) (functor, 1 - terminal category, U(0) - topos)
Bool : Obj(U(0)) (object)
true : 1 -> Bool (arrow)
false : 1 -> Bool

if_then_else_ : Bool -> Hom(T x T, T)
if_then_else_ . true => first (2-arrow)
if_then_else_ . false => second

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

А насчёт

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

Но зачем мне выходить за пределы своего узкого кругозора? Чтобы понять собеседника? Тогда как на что я должен смотреть на сложные выражения (какие?) языка (какого?)?

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

BASIC & Python.

будут типы для отдельных значений, тем, что это В АГДЕ НЕ ВЫРАЖАЕТСЯ!

Не, это нигде не выражается и глупость само по себе. Когда ты в Racket пишешь 5 на месте типа ты на самом деле имеешь в виду множество {5} или, допустим, предикат который true на месте 5 и false везде вокруг (где? XIX век что ли). В любом хаскеле это будет любой обычный тип с одним конструктором 5 - подтип Integer. А именно терм 5 как тип это, в крайнем случае, домен/кодомен 2-стрелки которая может задавать правило переписывания или ещё что-то - не принято называть «тип».

В хаскеле над/подтипов нет

Int - подтип (forall (a :: *). a), подтип (forall (a :: *). Num a => a), подтип (forall (a :: *). Integer :> a => a).

В любом хаскеле это будет любой обычный тип с одним конструктором 5 - подтип Integer.

{-# LANGUAGE TypeOperators, MultiParamTypeClasses, FunctionalDependencies
  , FlexibleInstances, UndecidableInstances #-}

class a :> b | a -> b, b -> a where
  sub :: a -> b
  sup :: b -> a
  ($>) :: (b -> c) -> a -> c
  ($>) f = f . sub
  (<$) :: (a -> c) -> b -> c
  (<$) f = f . sup
  (<$>) :: (a -> a) -> b -> b
  (<$>) f = sub . f . sup
  (>$<) :: (b -> b) -> a -> a
  (>$<) f = sup . f . sub

data Five = Five

instance Num a => a :> Five where
  sup Five = 5

test :: Five -> Integer -> Integer
test = (<$) (+)
-- ^ test Five 10 => 15

И там сделано так, что строки можно использовать на тех местах где ожидается Data, потому что определено соответствующее преобразование String -> Data

ну вот именно. там не используется data. там используется data, которое автоматически приводится к нужному типу. А использовать data в качестве другого типа хаскиль не умеет. только автоматически приводить.

Хочешь сказать, что в модельной категории у стрелок нет объектов? Или что в модельных системах типов из TAPL/ATTAPL/whatever все правила формирования _типов_ для сложных _выражений_ это ни о чём?

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

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

Да нет, все совершенно не так. еще раз, для особо одаренных, сперва мы имеем НАБЛЮДАЕМЫЕ типы. Это нам дано. И потом мы пытаемся смоделировать эти наблюдаемые типы путем правил. нам не надо ничего придумывать. Как значения перечисляются, как составляются сложные выражения и как составляются типы - это нам все дано. Это все не зависит от нас и мы на это никак не можем повлиять. Мы можем лишь попытаться смоделировать эти аспекты (с той или иной степенью успеха).

Но зачем мне выходить за пределы своего узкого кругозора?

Чтобы понимать, о чем говоришь. Ваше взращенное на абстракциях поколение повторяет раз прочитанные формулировки теорем, определений, утверждений, но не понимает ни откуда они взялись, ни что они значат, ни почему они такие, какие есть. Естественно, создать ничего нового таким образом нельзя. Абстракция вообще не может создать ничего нового. Вообще, на мой взгляд, очень хороший вопрос для человека на понимание современной математики: «почему в рамках теории категории не сформулировано ни одного нового результата?». Если человек не в состоянии ответить на этот вопрос - он не понимает фундаментальных вещей и является вышеупомянутым попугаем. Самое страшное, что большинство не то что на этот вопрос ответить не может - оно даже начинает в ответ утверждать, что новые результаты в рамках теорката были! То есть явно человек не понимает что такое теоркат и как он работает.

Надеюсь, это не просто апелляция к математике, где с помощью значка 5 я действительно могу обозначать что угодно

Нет, наоборот. Это апелляция к тому, что число «5» не является неким абстрактным символом, удовлетворяющим абстрактным свойствам. Это апелляция к тому, что число «5» - это некий объект, который нам изначально дан, который обладает свойствами, которые нам изначально даны. И все те самые абстрактные теории - лишь попытки смоделировать тот самый объект. Они не стоят вначале. Они - лишь побочный эффект. И не имеют ценности сами по себе. Так же как определение группы не имеет ценности само по себе - совокупность преобразований некоторого множества является группой, потому что именно такие преобразования и исследовались изначально. И эти аксиомы - _свойства_ (наблюдаемые, данные нам и от нас не зависящие) этих преобразований. Эти свойства пытались отыскать для исследований и нашли. А теорема о том, что любая группа изоморфна группе преобразований утверждает лишь тот факт, что свойства были определены _точно_ (то есть модель корректна). Чего не скажешь о той же топологии, например - изначально это наука, которая должна была стоять «в фундаменте» анализа. Но потом выяснилось, что для анализа надо наделить топ. пространство еще и гладкой структурой - и вот аксиоматика гладкой структуры уже была корректной моделью, т.к. любое дифф. многообразие есть подмногообразие обычного комплексного многообразия той же размерности.

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

Ну вот о чем я и говорил. То есть человек просто себе даже и представить не может, что что-то может быть НЕ ТАК КАК В ХАЦКИЛЕ. Это непробиваемо. То есть вот прям перед ним есть корректная, непротиворечивая система типов, в которой это возможно (а самое смешное, что это и в том же хаскеле в принципе возможно и в агде, формализм не запрещает, - но товарищ просто тупо даже одного логического шага сделать не может), которую можно пощупать, которая актуально существует и дана нам в ощущениях - но товарищ говорит «не знаю, не вижу не слышу, и вообще я в домике», то есть как будто перед ним ничего нет. Как с такими разговаривать, не переходя в «заносы в сторону»? То есть казалось бы - уже не раз и подробно объяснил, что весь его хацкиль с таплом и агдой - это даже не верхушка айсберга, это одна песчинка из этой верхушки. И кроме этой теории есть еще куча других, ничем не хуже. Но товарищ с истинно религиозным упорством заводит на который раз свое «ежи еси на небеси ...».

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

Когда ты в Racket пишешь 5 на месте типа ты на самом деле имеешь в виду множество {5} или, допустим, предикат который true на месте 5 и false везде вокруг (где? XIX век что ли)

Именно так. В этой модели тип - это некое множество, которое мы можем определить при помощи предиката. Эта модель теоретически обоснована не хуже чем хацкельская, она даже лучше обоснована и красивее - у нее и история больше и исследована она лучше (де-факто вся математика, не только CS, занимается изучением этой модели), так мало того - она еще и лучше отражает реальные типы, то есть корректнее! Но нет - из религиозных соображений ты будешь долбиться в жопу лямбда-кубом (кстати, даже рамках _твоих_ представлений, в рамках всякого теорката, системы лямбда-куба - это лишь один единственный класс систем, а есть и другие, много более выразительные, но куда тебе это знать, тут парой статеек про мондады не обойдешься ...). Потому что ничего друго для тебя нет. то есть на практике (и в CS-теории) оно есть, но нахватавшийся по верхам скажет «я в домике!» и на этом конец.

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

nt - подтип (forall (a :: *). a), подтип (forall (a :: *). Num a => a), подтип (forall (a :: *). Integer :> a => a)

Еще раз для особо одаренных - В ХАСКЕЛЕ НЕТ ПОДТИПОВ. Int - это не подтип «forall (a:: *) a», а элемент кодомена соответствующей функции над типами (любой полиморфный тип - функция над типами). А тебе я бы советовал прочитать TAPL и узнать, что такое «подтип».