Архитектура системы верификации кода драйверов Linux

> 3 -> (* whatever *);

end

у тебя, как видишь, ошибка (неполный набор вариантов матчинга); компилятор ее тебе выдаст?

> компилятор ее тебе выдаст?

Не знаю. Но я знаю, что в Си он ее не выдаст.

> Не знаю. Но я знаю, что в Си он ее не выдаст.

а бласт будет выдавать

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

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

> бласт в текущем варианте ее, возможно, не выдаст, но если дописать к нему соответсвующую простенькую теорию, то выдаст обязательно

Ну так гипотетический компилятор Ocaml тоже ее выдаст. И даже напрягаться сильно не придется.

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

Ты ХЗ сколько времени рисуешь чудовищные конструкции и называешь их паттерн-матчингом. А простая истина в том, что паттерн-матчинг умеет всё, что switch, и еще дофига всего.

> Ну так гипотетический компилятор Ocaml тоже ее выдаст. И даже напрягаться сильно не придется.

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

> «гипотетический компилятор Ocaml» проектировался в расчете на то, что кто-то будет добавлять к нему возможности проверять полноту матчинга

Реальный компилятор Ocaml уже проверяет полноту матчинга. Достаточно ли он умен, чтобы понять, что значение 0..4 - хз.

> А простая истина в том, что паттерн-матчинг умеет всё, что switch, и еще дофига всего.

switch при наличии SMT-solver-а умеет все что паттерн-матчинг, и намного приятнее и надежнее, правда его требуется как-то согласовать с обычными АлгТД

> switch при наличии SMT-solver-а умеет все что паттерн-матчинг

Правда? А матчинг по чему-то более сложному, чем целые числа, он умеет?

> Ты ХЗ сколько времени рисуешь чудовищные конструкции и называешь их паттерн-матчингом.

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

после того, как экономия стала ясна, ты вернулся к моему варианту и стал именовать мой свитч частным случаем паттерн матчига

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

1. паттерн-матчинг позволяет вводить новые переменные с областью видимости ветки *на основе выполнения гварда, защищающего ветку* — заметь, у меня в свиче они не вводятся (хотя вводятся в функциях f1,f2,f3)

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

> Правда? А матчинг по чему-то более сложному, чем целые числа, он умеет?

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

> после того, как экономия стала ясна, ты вернулся к моему варианту

После того, как я понял твою странную задачу.

и стал именовать мой свитч частным случаем паттерн матчига

И выступил в роли КО. Кстати, ты не поверишь... любой switch, не только твой - это убогий паттерн-матчинг.

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

0. Умеет работать со сложными структурами данных.

1. паттерн-матчинг позволяет вводить новые переменные с областью

2. паттерн-матчинг обычно проверяется компилятором

fixed

> множество АлгТД счетно, так что матчинг по ним это матчинг по целым числам

А еще есть паттерн матчинг по спискам.

в хаскеле, во всяком случае, паттерн-матчинг по спискам ничем не отличается от ПМ по АлгТД (разве что синтаксисом)

Тут у тебя «простой и ясный код» потому что f1-f3 могут применять нулевые указатели - но внутри они же должны делать выбор что у них ненулевое? Это и будут дополнительные варианты - просто матчинг разнесен в 4 функции.

Здесь

case (Just(aa), Nothing, Nothing, Nothing),
         (Nothing, Just(aa), Nothing, Nothing),
         (Nothing, Nothing, Just(aa), Nothing),
         (Nothing, Nothing, Nothing, Just(aa)): return h1(x, aa);

ты хочешь найти aa любой - но это же не так в f1..f3?

Потому что в этом случае можно описанный мной выше flat применить к списку из четырех Мейби значений и получить нормализованный список по Just a, и сделать 5 вариантов матчинга

 case a :: b :: c :: d => 
 case a :: b :: c => 
 case a :: b  => 
 case a  => 
 case Nil  => 

А если надо будет exhaustiveness check - то надо сгенерировать 22 подобных класса (это для 2х значений):

 sealed abstract class OptionTuple2[+T];

object OptionTuple2 {
	def apply[T](x:Option[T],y:Option[T]):OptionTuple2[T] = (x, y) match {
		case (Some(x), Some(y)) => OT2_2(x,y);
		case (Some(x), None) => OT2_1(x);
		case (None, Some(y)) => OT2_1(y);
		case (None, None) => OT2_Nothing;
	}
}

case object OT2_Nothing extends OptionTuple2[Nothing];
case class OT2_2[T](x:T,y:T) extends OptionTuple2[T];
case class OT2_1[T](x:T) extends OptionTuple2[T];

>А если надо будет exhaustiveness check - то надо сгенерировать 22 подобных класса (это для 2х значений):

Или Dependent Types.

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

Да, не заметил.

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

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

и обязательно он должен давать ошибки на варианты

В агде, например:

cn : Ref⁺ → Ref⁺ → Fin 3

test : Ref⁺ → Ref⁺ → _

test a b with cn a b
... | zero = _
... | suc zero = _
... | suc (suc zero) = _
... | _ = _

Ok

test a b with cn a b
... | zero = _
... | suc (suc zero) = _
... | suc (suc (suc _)) = _

Incomplete pattern matching for .M.with-19. Missing cases:
  .M.with-19 _ _ (suc {._} (zero {._}))

test a b with cn a b
... | zero = _
... | suc zero = _
... | suc (suc zero) = _
... | suc (suc (suc _)) = _
... | suc (suc (suc (suc _))) = _

ℕ.suc n != ℕ.zero of type ℕ
when checking that the pattern suc _ has type Fin ℕ.zero

test a b with cn a b
... | zero = _
... | suc zero = _
... | suc (suc _) = _
... | suc (suc (suc _)) = _

Unreachable clause

насчёт null pointer access:

Data : Set
Data = _

Address : Set
Address = _

record Null : Set where
  constructor null

record Ref : Set where
  constructor ref
  field
    address : Address
    value   : Data

Ref⁺ : Set
Ref⁺ = Null ⊎ Ref

т.е. value : Ref → Data а *не* value : Ref⁺ → Data, так что доступа к данным по null pointer-у не может быть вообще.

опять же, надо чтобы можно было написать

Ещё раз - весь код который ты тут пишешь использует только такие сишные конструкции как функции, операторы, if и switch. Те же самые конструкции есть и в хаскеле и в agde и где угодно. Почему ты думаешь, что весь этот код не может выглядеть там точно также (в хаскеле - функции/операторы = ленивые функции, if = if, switch = case)? Он так и будет выглядеть и паттерн-матчинг тут ни при чём.

Вот если бы тут были примеры с присваиванием, goto или longjump или, скажем, с тредами и IPC, это бы потребовало бOльших усилий, т.е. разработки _моделей_ выполнения с присваиванием, или goto, или longjump, или моделей многопоточных программ с расшаренной памятью. В хаскеле такие модели настраиваются с помощью монад (IO (или RWS), Cont, STM), хотя вообще могут быть определены непосредственно - заданием синтаксиса и статической семантики.

Я тут призывал к тому, чтобы точно зафиксировать типы (отделить мух от котлет) для чисел разной разрядности (причём в духе Fin (2 ^ n) из агды), для целых, натуральных и булевых чисел, для индексов, адресов, указателей, нулевых указателей и т.д. и т.п. Тогда в хорошо типизированном языке (adts + strong + static + well-typed) все упомянутые проблемы (null pointe-ов, покрытия и достижения всех clauses) отпадут сами собой.

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

тут вообще-то можно было бы возразить, что множество АлгТД счетно

Строки это АлгТД? Множество всех строк счётно?

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

Могу сказать, что любая нормальная реализация ML-я или haskell-я (например, GHC с -Wall) умеет полноту матчинга для ADT. Но они не умеют полноту матчинга для, например, чисел, т.к. числа там примитивные а не алгебраические типы.

В агде есть алгебраические числа (натуральные в виде чисел Пеано, целые со знаком) и зависимые типы для множеств с конечным числом элементов. Например, тип (Fin 3) это тип ровно из трёх элементов, поэтому, если делать по нему паттерн-матчинг, он не отстанет, пока не напишешь всех случаев - для 0, 1 и 2, причём в правильном порядке.

не умеют полноту матчинга для, например, чисел

Хотя, у GHC есть какие-то эвристики на эту тему:

t n = case n of { 1 -> 1; 2 -> 2; 3 -> 3; 5 -> 5 }

    Warning: Pattern match(es) are non-exhaustive
             In a case alternative:
                 Patterns not matched: #x with #x `notElem` [1#, 2#, 3#, 5#]

Я тут призывал к тому, чтобы точно зафиксировать типы (отделить мух от котлет) для чисел разной разрядности (причём в духе Fin (2 ^ n) из агды), для целых, натуральных и булевых чисел, для индексов, адресов, указателей, нулевых указателей и т.д. и т.п. Тогда в хорошо типизированном языке (adts + strong + static + well-typed) все упомянутые проблемы (null pointe-ов, покрытия и достижения всех clauses) отпадут сами собой.

ыыы!

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

f n = case (n*n) `mod` 4 of { 0 -> 0 ; 1 -> 1; 2 -> 99; 3 -> 99 }

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

> Я тут призывал к тому, чтобы точно зафиксировать типы (отделить мух от котлет) для чисел разной разрядности (причём в духе Fin (2 ^ n) из агды), для целых, натуральных и булевых чисел, для индексов, адресов, указателей, нулевых указателей и т.д. и т.п. Тогда в хорошо типизированном языке (adts + strong + static + well-typed) все упомянутые проблемы (null pointe-ов, покрытия и достижения всех clauses) отпадут сами собой.

этого *недостаточно*

1. пусть у нас есть корректная програма на си (корректность понимаем так, что она никогда не разыменовывает нулевые указатели)

2. пусть мы эту программу переписываем с МауВе, или вообще с АлгТД, и при этом обязательно требуется:

2А. либо тонна бойлерплейта, возможно чуток обобщенная и вынесенная с глаз долой в отдельный файл (как это предлагает r)

2В. либо отход от естественного порядка написания программы (пример: если специфика предметной области подталкивает к тому, чтобы отдельно рассматривались именно случаи 0,1,2,3,4 ненулевых указателя, а не все 16 отдельных комбинаций)

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

тут должнен бытье еще пункт

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

я раскрою его постом ниже

(это на тему 2С, см. выше)

l.flatMap(x=>x).foldLeft(0)(_ + _);

до меня наконец дошла твоя идея

в принципе да, мы можем написать

int zero_if_nothing(maybe<int> t) { 
  switch(t){
    case Nothing: return 0;
    case Just(tt): return tt;
  }
}

int f( maybe<int> a, maybe<int> b, maybe<int> c, maybe<int> d )

  int x = g();

  switch( is_just(a) + is_just(b) + is_just(c) + is_just(d) ) {
    case 0: return x;
    case 1: return f1(x, a, b, c, d);
    case 2: return f2(x, a, b, c, d);
    case 3: return f3(x, a, b, c, d);
    case 4: return x + zero_if_nothing(a) + zero_if_nothing(b) + zero_if_nothing(c) + zero_if_nothing(d);

}

для того, чтобы компилятор заткнулся со своими ошибками

но тут проблемы:

* для сложения нужно zero_if_nothing, для умножения нужно one_if_nothing, для каких-то операций может вообще не быть нейтральных элементов, и тогда код становится совсем стремным (грозящим неправильным рефакторингом)

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

ну или в «си с обязательными проверками перед разыменованием» это же могло бы выглядеть так:

int f(int* a, int* b, int* c, int* d)
{
  int x = g();

  switch( !!a + !!b + !!c + !!d ) {
    case 0: return x;
    case 1: return f1(x, a, b, c, d);
    case 2: return f2(x, a, b, c, d);
    case 3: return f3(x, a, b, c, d);
    case 4: return x + (a ? *a : 0)+ (b ? *b : 0) + (c ? *c : 0) + (d ? *d : 0);
  }
}

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

>* для сложения нужно zero_if_nothing, для умножения нужно one_if_nothing,

Или делаются эти операции для мейбитипов или переход от обработки пары выражений к переходу к обработке списков выражений. Тут ведь суть в том что тот же Maybe переводит в се в логику «значения может и не быть» не потому что это языковой выпендреж а потому что его действиетльно может не быть, и переход в обычные скаляры - это либо грязный тайпкаст - потенциальный исключение, либо необработанный вариант 'который никогда не будет' - вообще внекодовое непроверяемое компилятором решение, либо 'скаляризация'. fold - это скаляризация. Первые два - потенциально некорректная пограмма, по меньшей мере в общем случае.

т.к. выражение сделано работающим там, где оно работать не должно

Как работают f1..f3? Потому что я как-то с трудом представляю что эта программа может делать, ведь в случае (Just a, Nothing, Nothing, Nothing) и (Nothing, Just b, Nothing, Nothing) вызывается один и тот же f1, но с разными аргументами. Тут или взаимноисключающая логика подразумевается с выбором внутри f1..f3, или тогда все a..d можно обрабатывать как список значений - а тут уж списочные операции в руки.

Тут у тебя «простой и ясный код» потому что f1-f3 могут применять нулевые указатели - но внутри они же должны делать выбор что у них ненулевое? Это и будут дополнительные варианты - просто матчинг разнесен в 4 функции.

т.е. у тебя тоже сомнения, что мой свич че-то экономит?

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

вот пример, который использует расширение си — си с ограниченными локальными функциями, которые, почти что не отличаются от define

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

int f(int* a, int* b, int* c, int* d)
{
  int x = g();

  // возращают значения по первому, последнему, и среднему ненулевому указателю из указателей в последовательности a, b, c, d
  int first() { return a ? *a : b ? *b : c ? *c : *d ; }
  int last()  { return d ? *d : c ? *c : b ? *b : *a ; }
  int middle(){ return (!a || !b) ? *c : *b; }

  switch( !!a + !!b + !!c + !!d ) {
    case 0: return x;
    case 1: return h1( x, first() );
    case 2: return h2( x, first(), last() );
    case 3: return h3( x, first(), middle(), last() );
    case 4: return x + *a + *b + *c + *d;
  }
}

тут аналогия с ПМ доведена до конца в одном куске кода

тут может быть возражение, что *сразу* надо было писать h1, h2, h3, и не запутывать ситуацию с f1, f2, f3, которым могут передеваться нулевые указатели

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

Тут или взаимноисключающая логика подразумевается с выбором внутри f1..f3, или тогда все a..d можно обрабатывать как список значений - а тут уж списочные операции в руки.

насчет списочных операций

пусть a..d это полученные (или неполученные) экспериментальные значения

когда их 4 штуки, мы можем по ним построить кривую методом наименьших квадратов, и обсчитать все что мы хотим с достаточной точностью

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

так что списочные операции пролетают

кстати, моя ошибка — надо было написать

case 0: return x-100;

чтобы неповадно было обращаться с ними как со списком

и case 4: return x + *a + *b + *c + *d; я тоже зря сделал таким простым

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

Но это же списочная обработка? Незачем их обрабатываьт позиционно - там сверху было как их обработать списком - тоже пять вариантов на паттерн матчинге. Ну а exhaustiveness check - dependent types.

>так что списочные операции пролетают

Независимые от длины списка. Зависимые - нет.

чтобы неповадно было обращаться с ними как со списком

«кусок кода 2» все еще валиден и паттерн матчинг на 5 значений
Архитектура системы верификации кода драйверов Linux (комментарий)

> «кусок кода 2» все еще валиден и паттерн матчинг на 5 значений Архитектура системы верификации кода драйверов Linux (комментарий)

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

кстати, я рассматривал мысль сделать аналогичный вариант на с++11, где один шаблон может вызываться с любым вариабельным количеством аргументов (а не от 0 до 22 :-)

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

> «кусок кода 2» все еще валиден и паттерн матчинг на 5 значений Архитектура системы верификации кода драйверов Linux (комментарий)

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

но оценка языка, по-моему, отсюда следует однозначная

>> так что списочные операции пролетают

Независимые от длины списка. Зависимые - нет.

от того, что ты назовешь любые 0..4 целых чисел списком, формулы для h1, h2, h3 одинаковыми («списочными») не станут — я это имел в виду

> от того, что ты назовешь любые 0..4 целых чисел списком, формулы для h1, h2, h3 одинаковыми («списочными») не станут — я это имел в виду

Зато с DT появится exhaustive PM и полиморфизм по длине.

DT = ?

> и полиморфизм по длине.

полиморфизмы по длине разные бывают

бывает полиморфизм в стиле шаблонов (для каждой длины свой код), а бывают в стиле дженериков (пофиг длина! делай вот это)

dependent types

ыыы!

Ну что смешного, поделись? :)

Ты тут путаешь (как и я в этом треде чуть раньше). unreachable code != unreachable clause. unreachable clause это нечно весьма определённое, но вместе с зависимыми типами (вроде Fin) оно может дать всё что нужно для доказательства отсутсвия unreachable code (естесвенно, _доказывать_ придётся руками).

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

Fin 2. Надо доказать, что f : ℕ → Fin 2.

кстати, интересно было бы на него взглянуть

Тут, например, можно посмотреть как подобные вещи там делают - http://www.cse.chalmers.se/~nad/repos/lib/src/Data/Nat/DivMod.agda

этого *недостаточно*

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

переписываем с МауВе, или вообще с АлгТД

Само произношение «АлгТД» забавное :) Но это же всё частности которыми не исчерпывается то что умеют математизированные ЯП.

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

либо отход от естественного порядка написания программы (пример: если специфика предметной области подталкивает к тому, чтобы отдельно рассматривались именно случаи 0,1,2,3,4 ненулевых указателя, а не все 16 отдельных комбинаций)

Это вообще не понятно. Весь код в твоих примерах настолько прост, что его и переписывать не нужно, проблема только в том, что это ill-typed код, прежде чем о чём-то говорить нужно хотя бы сделать код хорошо типизированным.

> Строки это АлгТД? Множество всех строк счётно?

ты спрашиваешь то, что знают все первокурсники

пусть алфавит конечен

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

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

(вообще память у компьютера ограничена, так что множество строк конечно, но так как досчитать даже до 10^50 мы не можем, то такие числа лучше рассматривать как принадлежащие к счетному множеству)

пусть алфавит конечен

А если нет? Например, такой ADT как [ℕ] счётный?

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

Ну хорошо,

ℕ = 0 | s ℕ
|ℕ| ≡ ℵ₀

[a] = [] | a : [a]
if |a| < ℵ₀ then |[a]| = ℵ₀
if |a| = ℵ₀ then |[a]| = 2 ^ ℵ₀ ≥ ℵ₁

> А если нет? Например, такой ADT как [ℕ] счётный?

а если подумать?

понятно, что теоремы можно и забыть, но ведь очевидно, что любой его элемент записывается в виде строки над конечным алфавитом, например 375:1900287:7:12:22

> |[a]| = 2 ^ ℵ₀

2 ^ ℵ₀ это все подмножества натурального ряда, тогда как [a] это только конечные

естественно, это все написано про не-ленивые языки

в случае лени у тебя кроме хвоста из настоящих натуральных чисел может стоять thunk, множество которых тоже счетно

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

если система типов твоего языка не может доказать корректность корректного конкретного кода (это ты называешь ill-typed код?), то это проблемы твоего языка и его создателся, а не мои

по агде есть конкретный вопрос

пусть у меня есть мегабайтовый исходник с каким-то кодом, в нем есть 2 строки

f::Int->Int
f n = case (n*n) `mod` 4 of { 0 -> 0 ; 1 -> 1; 2 -> 99; 3 -> 99 }

напускаем на это допустим агду

1. выдаст ли она «варнинг: недостижимый код»?

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

или может переопределить, оператор `mod` или может быть оператор умножения  — но при этом запрещается менять саму функцию

> Тут, например, можно посмотреть как подобные вещи там делают - http://www.cse.chalmers.se/~nad/repos/lib/src/Data/Nat/DivMod.agda

ты сунул мне кусок стандартной библиотеки агды, и зачем?

давай приведи конкретный код, который бы агда съела, ругнулась на недостижимый код в f, и успокоилась бы после удаления лишних ветвей

> Ты тут путаешь (как и я в этом треде чуть раньше). unreachable code != unreachable clause. unreachable clause это нечно весьма определённое,

раскрой пожалуста подробнее смысл этого «нечно весьма определённого», смысл недостижимого кода и докажи, что unreachable code != unreachable clause

А если нет? Например, такой ADT как [ℕ] счётный?

а если подумать?

То что [ℕ] несчётный это то что Кантор доказывал (про действительные числа и диагональный аргумент).

2 ^ ℵ₀

Множество с такой мощностью это, как минимум, несчётное множество (вне зависимости от CH, причём).

тогда как [a] это только конечные

[a] это:

[a] ::= [] | a [a]

т.е. и бесконечные тоже.

Правда, вопрос о том сколько (ℵ₀, 2 ^ ℵ₀, ℵ₁, ... ?) неизоморфных ADT можно задать с помощью метаязыка задания ADT (т.е. типы суммы от от типов произведений) несколько сложнее. Твой изначальный посыл был, вроде, в том, что множество ветвей у switch/case счётно, что верно, т.к. часть грамматики ADT про вариантные типы такая:

type_sum ::= type_prod | type_prod type_sum

т.е. количество вариантов счётное.

корректность корректного конкретного кода

КККК? Я что-то плохо понимаю, уже поздно, наверно. Но:

если система типов твоего языка не может доказать

Какая система типов какого языка? Вообще, пусть будет хоть какая-то _система_ типов (т.е. формальная и непротиворечивая), чем её не будет вообще (как в си). Пусть будет система типов хотя бы как в Cyclone. Доказательства корректности это уже другой вопрос.

это ты называешь ill-typed код?

Это около-хаскельное понятие, ill-typed это всё что не well-typed, а well-typed язык это язык с заданной формальной и непротиворечивой статической семантикой.

ты сунул мне кусок стандартной библиотеки агды, и зачем?

Чтобы ты посмотрел тип _mod_ и то почему у неё именно такой тип.

раскрой пожалуста подробнее смысл этого «нечно весьма определённого», смысл недостижимого кода и докажи, что unreachable code != unreachable clause

Пожалуй, не буду этого делать. Ну, то есть, one всегда может заняться самообразованием :)

по агде есть конкретный вопрос

Напиши функцию squere_mod_4 : Integer -> Fin 2 и замени case (n*n) `mod` 4 of на case squere_mod_4 n of (в агде это будет не case а with), тогда скомпилируется только { 0 -> _ ; 1 -> _; } и ничего другого. При этом f останется совместимой со всем остальным кодом.

На хаскеле это будет так (чтобы пояснить идею):

{-# LANGUAGE GADTs, KindSignatures #-}

data Z
data S n

class N t
instance N Z
instance N n => N (S n)

type N0 = Z
type N1 = S N0
type N2 = S N1
-- ...

data Fin :: * -> * where
  Zf :: N n => Fin (S n)
  Sf :: N n => Fin n -> Fin (S n)

unproven :: a
unproven = error "totality is not proven."

unreachable :: a
unreachable = error "unreachable code."

square_mod_4 :: Int -> Fin N2
square_mod_4 n = case (n * n) `mod` 4 of
  0 -> Zf
  1 -> Sf Zf
  _ -> unproven

f :: Int -> Int
f n = case square_mod_4 n of
  Zf    -> 0 
  Sf Zf -> 1
  _     -> unreachable

слишком вербозно и без возможности доказать тотальность функций.

> т.е. и бесконечные тоже.

я уже сказал, что рассматриваю не-ленивые языки, и там это конечные

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

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