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

> Чего вы прицепились к проверке указателя на NULL? Это банальщина.

потому и прицепился, что это банальщина, епрст! разве не понятно?!

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

а что будет, если продолжить *этот* подход дальше? если отвечать с некоторым пафосом и некоторой натяжкой — получим тот тупик, куда движутся современные языки программирования

Изобразите

кое-что я могу изобразить с помощью зависимых типов, а вот насчет запрета kmalloc(*, GFP_KERNEL) надо подумать

>> switch( !!a + !!b + !!c + !!d )

Вот лично я не понял, что проверяет эта «простая и ясная» проверка.

код *считает* количество ненулевых указателей среди a b c d, и в зависимости от этого выполняет одну из веток свича

корректность/проверка этого кода состоит в том, что

1. в любой ветке не разыменовываются нулевые указатели

2. при всех вариантах нулевых и не-нулевых указателей функция таки возвратит целое (т.е. все варианты рассмотрены)

ыыы! твои простыни невозможно читать

у меня конкретный вопрос: можно ли как-то сделать, чтобы в паттерн-матчинге было не 16 веток, а 5 как у меня?

но я все же почитаю и выскажусь

у меня конкретный вопрос: можно ли как-то сделать, чтобы в паттерн-матчинге было не 16 веток, а 5 как у меня?

Во-первых, да. Смотри пост, там где test a b c d = ... Похоже на сишный же код? Во-вторых, и тут простыня про паттерн-матчинг и его незначительную роль, а ну я об этом писал уже :)

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

а что будет, если продолжить *этот* подход дальше?

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

Я тут подумал, что это за эмоция у меня возникает глядя на такое непонимание со стороны людей, которые, вроде бы, любят и статические системы типов и верификацию времени компиляции? Не иначе как facepalm :)

Не совсем понял этот пример (что мы тут верифицируем?).

1. в любой ветке не разыменовываются нулевые указатели

2. при всех вариантах нулевых и не-нулевых указателей функция таки возвратит целое (т.е. все варианты рассмотрены)

и еще желательно

3. тут нет unreachable code

в качестве аналога, видимо, предлагается намного более простая вещь чем у тебя — пусть у нас вместо возможно-нулевых-указателей есть объекты класс Option[int] (если мы рассматриваем скалу) или MayBe Int (если хаскель)

задача: у нас есть 4 объекта АлгТД MayBe Int

нам надо сделать разные действия в зависимости от количества среди них Nothing (или Just, не важно)

при этом 1, 2, 3 должно проверяться компилятором

допустим, что is_just проверяет на то, что у нас Just, и выдает целое 0 или целое 1

тогда написать

case is_just(a) + is_just(b) + is_just(c) + is_just(d) of
    0 -> x
    1 -> x -- f1 ...
    2 -> x -- f2 ...
    3 -> x -- f3 ...
    4 -> x +. a +. b +. c +. d

мы, как я понимаю, не можем, т.к. x +. a +. b +. c +. d будет типа MayBe Int, так?

з.ы. если бы у нас были шаблоны в хаскеле, то is_just мог бы выдавть MySuperBoolean<1>, дальше сумма объектов MySuperBoolean<3> и MySuperBoolean<1> имела бы тип MySuperBoolean<3+1>, и мы бы поимели полноту матчинга — но заданный чуть выше вопрос это не снимает

> Не иначе как facepalm :)

не все так просто

> Не иначе как facepalm :)

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

s/MayBe/Maybe/

надеюсь, все равно всем понятно

1. в любой ветке не разыменовываются нулевые указатели

Указатели как maybe-подобный тип + тотальные функции = нулевые указатели никогда не разыменовываются.

2. при всех вариантах нулевых и не-нулевых указателей функция таки возвратит целое (т.е. все варианты рассмотрены)

И GHC и agda умеют выводить тотальность. GHC кидает ворнинги (при -Wall), а agda вообще запрещает частичные функции.

3. тут нет unreachable code

В аппликативном программировании нет unreachable code как класса.

предлагается намного более простая вещь чем у тебя ... MayBe Int

У меня как раз это (там есть комментарий про изоморфизм с Maybe Integer, лишняя специфичность тут не помешает).

тогда написать

Лучше так:

countNull :: [Ptr] -> W
countNull = sum . map fn
  where
    fn :: Ptr -> W
    fn = (cast :: B -> W) . (cast :: Ptr -> B)

test a b c d =
  let x = Ptr 777 in
  case countNull [a, b, c, d] of
    0 -> x
    1 -> x
    2 -> x
    3 -> x
    4 -> x +. a +. b +. c +. d

мы, как я понимаю, не можем, т.к. x +. a +. b +. c +. d будет типа MayBe Int, так?

Как я это написал - определил операцию (+.) для типа Ptr. Но не очень думал - какова семантика bad_pointer + (good_pointer x)?

А вообще, смысл конструкции (a + b), где a и b - указатели на int в студию. Я понимаю там сдвиг указателя данное количество байт вверх/вниз, но это.

-- | Pointer arithmetic.
class PtrArith t where
  -- | Shift of a pointer.
  (+.) :: t -> N -> t
  -- | Etc.
  -- ...

instance PtrArith Ptr where
  Null  +. _ = Null
  Ptr x +. y
    | x + y < maxOf word = Ptr $ x + y
    | otherwise          = Null

если бы у нас были шаблоны в хаскеле

Зачем в хаскеле шаблоны? Параметрический полиморфизм, ad-hoc полиморфизм, макросы - всё это покрывается естественными для хаскеля средствами.

как у тебя получается убрать MayBe

Убрать maybe? В смысле. В том коде Prt ~ Maybe Integer.

> Как я это написал - определил операцию (+.) для типа Ptr. Но не очень думал - какова семантика bad_pointer + (good_pointer x)?

это ключевой момент (и не нужно простыней, да)

дело в том, что когда у нас is_just(a) + is_just(b) + is_just(c) + is_just(d) == 4, то тогда *все* они хорошие указатели, и *каждый* из них можно превратить в int — bad_pointer-ов вообще нет

вопрос только в том, как ты это объяснишь компилятору хаскеля

не все так просто

Тут всё весьма просто.

а еще посмотри внимательно — у меня х это не указатель, а целое

В аппликативном программировании нет unreachable code как класса.

бугага

case x*x `mod` 4 of
  0 -> ...
  1 -> ...
  2 -> unreachable code
  3 -> unreachable code

это ключевой момент (и не нужно простыней, да)

Ну так какой ответ на цитируемый вопрос?

Если в сишке можно писать { int *a, *b; a + b } это не значит, что у этого a + b есть нормальная семантика. Я могу себе представить такие хорошие функции:

+ : Prt → ℤ → Ptr   -- shift
- : Ptr → Ptr → ℤ   -- offset

и всё.

дело в том, что когда у нас is_just(a) + is_just(b) + is_just(c) + is_just(d) == 4 то тогда *все* они хорошие указатели

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

sum : {n m : ℕ} → Vec Bool n → (m ≤ n)

бугага

Ах в этом смысле.

if (нашёл целые корни уравнения (x^n + y^n = z^n)) {
    ...
} else {
    ...
}

и давай теперь требуй инструмент статического анализа, который отсечёт unreachable code ;)

а еще посмотри внимательно — у меня х это не указатель, а целое

Это я понимаю (shift указателя), но не a + b + c + d. Смысл?

> Ах в этом смысле.

и давай теперь требуй инструмент статического анализа, который отсечёт unreachable code ;)

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

Может пояснишь, какие другие смыслы есть?

Я подумал было на требование от функций быть тотальными. Т.е. покрытие кодом всех вариантов у данного вариантного типа. Ну и невозможность написать код который бы не был аппликацией/абстракцией/локальной специальной формой.

> Я подумал было на требование от функций быть тотальными. Т.е. покрытие кодом всех вариантов у данного вариантного типа. Ну и невозможность написать код который бы не был аппликацией/абстракцией/локальной специальной формой.

Т.е. покрытие кодом всех вариантов у данного вариантного типа.

Опиши, что ты имел ввиду, на примере функции «const» в прелюдии хаскеля

Что я имел ввиду не имеет отношения к unreachable code, т.е. = моя тупость, в данном случае.

>> запрет использования kmalloc(*, GFP_KERNEL) из прерывания

Вот как раз, два параметрических типа IO и STM с линейными монадическими интерфейсами не могут смешиваться

Ты знаешь много умных слов, браво. Именно поэтому я просил тебя _изобразить_ решения задач, а не сказать «в Хаскелле это как два байта переслать».

У си не позволяет, по чисто историческим причинам (теоретически, нет причин по которым си не мог бы быть безопасным и иметь мощные типы).

Естественно, ты можешь придумать маленькое расширение Си или правило верификации (см. статью).

теоретически, нет причин по которым си не мог бы быть безопасным и иметь мощные типы

*короткая презрительная ругань* Когда уже кто-нибудь из теоретиков спустится с небес и хотя бы попробует сделать юзабельный безопасный Си?

> код *считает* количество ненулевых указателей среди a b c d, и в зависимости от этого выполняет одну из веток свича

Это как раз понятно (и случаи 0 и 4 тоже понятны). Но в 3 из 5 веток нельзя сделать никакого полезного вывода о поступивших аргументах.

Чего вы прицепились к проверке указателя на NULL? Это банальщина.

потому и прицепился, что это банальщина, епрст! разве не понятно?!

Непонятно. Это слишком тривиально, чтобы на этом примере продемострировать что-то полезное.

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

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

кое-что я могу изобразить с помощью зависимых типов,

Изобрази хоть что-нибудь полезное, а то этот топик стремительно скатывается в CS-мастурбацию.

> Это как раз понятно (и случаи 0 и 4 тоже понятны). Но в 3 из 5 веток нельзя сделать никакого полезного вывода о поступивших аргументах.

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

дальше, в зависимости от количества экспериментальных данных, мы, с должным запасом в сторону надежности, вычисляем *a+*b+*c+*d

например, если известно всего одно из них, скажем с, то надежно (надежно с точки зрения дальнейшего применения) можно считать, что сумма по крайней мере не меньше чем *с/10 + *с/5 + *с + *с/5

и так далее — т.е. каждая из функций f1, f2, f3 это такая приличная портянка с разбором случаев и комментариями, почему мы так решили, поэтому нам желательно сделать одну функцию f (в моем примере), которая будет наглядно отсылать к ним

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

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

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

1. я там недалеко упомянул про пафос и натяжки

2. «не для этого» — да, и это заставляет меня иметь пока не окончательное мнение

3. АлгТД недалеко ушли от этого узкого частного случая

Непонятно. Это слишком тривиально, чтобы на этом примере продемострировать что-то полезное.

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

Изобрази хоть что-нибудь полезное, а то этот топик стремительно скатывается в CS-мастурбацию.

1. не скатывается — квазимото известен тем, что постит простыни, когда надо задать вопрос, но это терпимо

2. изображать надо на чем-то; в с++ нет зависимых типов, но если (... простынка...) то можно считать, что они есть (компилятор будет это проверять, ... опять длинная простынка ...)

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

Это я понимаю (shift указателя), но не a + b + c + d. Смысл?

а ты си знаешь?

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

читай внимательно: x + *a + *b + *c + *d имеет тип «целое число», а не «указатель на целое»

Это довольно странный способ узнать об этом, но, кажется, ты хочешь доказать такое высказывание: sum : {n m : ℕ} → Vec Bool n → (m ≤ n)

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

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

  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 4: return f3(x, a, b, c, d); 
    case 3: return x + *a + *b + *c + *d; // null pointer access
  }
  switch( !!a + !!b + !!c + !!d ) { // incomplete switch
    case 0: return x;
    case 1: return f1(x, a, b, c, d);
    case 2: return f2(x, a, b, c, d);
    case 4: return x + *a + *b + *c + *d;
  }
  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 + *b + *c + *d;
    case 5: return x + 1; // unreachable
  }

> зависимости от количества экспериментальных данных, мы, с должным запасом в сторону надежности, вычисляем *a+*b+*c+*d

Если не проверишь их на NULL - сегфолт, если проверишь - твой неконвенционный switch не нужен.

каждая из функций f1, f2, f3 это такая приличная портянка с разбором случаев и комментариями

ну и что ты сэкономил своим switch?

Изобрази хоть что-нибудь полезное, а то этот топик стремительно скатывается в CS-мастурбацию.

1. не скатывается — квазимото известен тем, что постит простыни, когда надо задать вопрос, но это терпимо

Когда он делает это в темах «о языках вообще» - ладно, там люди понимающие. А здесь топик для приземленных драйверописателей. Если сказал «да, это можно» - приведи пример. Как говориться, картинка стоит тысячи слов.

2. изображать надо на чем-то; в с++ нет зависимых типов

Ну так придумай их.

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

int f1(int x, int* a, int* b, int* c, int* d)
{
  return x + ( !!a ? *a : !!b ? *b : !!c ? *c : *d )*3/2 ;
}

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

> Когда он делает это в темах «о языках вообще» - ладно, там люди понимающие. А здесь топик для приземленных драйверописателей.

нет уж

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

Если сказал «да, это можно» - приведи пример.

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

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

Я не желаю видеть примеры на Хаскеле. Я желаю видеть примеры на Си, возможно, расширенном зависимыми типами, или на Си и языке внешнего верификатора. Трёп на остальных языках рассматривается, но не убеждает.

> if (нашёл целые корни уравнения (x^n + y^n = z^n)) { и давай теперь требуй инструмент статического анализа, который отсечёт unreachable code

у нас же SMT-solver; варианты:

1. выдавать варнинг или ошибку, пока теорию, необходимую для этого уравнения, в SMT-solver не добавят

2. выдавать варнинг или ошибку, пока then-часть не помечена как «возможно недостижимая»

3. нашёл_целые_корни_уравнения это частичная функция?

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

3.2. если нет, то скорее всего из ее статического анализа видно, что она выдает и true и false

> Ну так придумай их.

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

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

потом я решил, что идея SMT-solver-а это то что надо, и тут, как видишь, бласт снова попался на глаза (правда, остается открытым вопрос, как его «согласовать» с общепринятой системой типов, с теми же АлгТД например)

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

> ну и что ты сэкономил своим switch?

щас напишу

ну и что ты сэкономил своим switch?

вот как это выглядело бы на си с паттерн-матчингом:

int h( maybe<int> a,  maybe<int> b,  maybe<int> c,  maybe<int> d)
{
  int x = g();

  switch( a ) {
    case Nothing:
      switch(b) {
        case Nothing:
          switch(c) {
            case Nothing:
              switch(d) {
                case Nothing: return x;
                case Just(dd): return h1(x, dd);
              }
            case Just(cc):
              switch(d) {
                case Nothing: return h1(x, cc);
                case Just(dd): return h2(x, cc, dd);
              }
          }
        case Just(bb):
          switch(c) {
            case Nothing:
              switch(d) {
                case Nothing: return h1(x, bb);
                case Just(dd): return h2(x, bb, dd);
              }
            case Just(cc):
              switch(d) {
                case Nothing: return h2(x, bb, cc);
                case Just(dd): return h3(x, bb, cc, dd);
              }
          }
      }
    case Just(aa):
      switch(b) {
        case Nothing:
          switch(c) {
            case Nothing:
              switch(d) {
                case Nothing: return h1(x, aa);
                case Just(dd): return h2(x, aa, dd);
              }
            case Just(cc):
              switch(d) {
                case Nothing: return h2(x, aa, cc);
                case Just(dd): return h3(x, aa, cc, dd);
              }
          }
        case Just(bb):
          switch(c) {
            case Nothing:
              switch(d) {
                case Nothing: return h2(x, aa, bb);
                case Just(dd): return h3(x, aa, bb, dd);
              }
            case Just(cc):
              switch(d) {
                case Nothing: return h3(x, aa, bb, cc);
                case Just(dd): return x + aa + bb + cc + dd;
              }
          }
      }
  }
}

отдельные функции h1,h2,h3 немного упрощаются, но это не оправдывает усложения функции h

int f1(int x, int* a, int* b, int* c, int* d)
{
  int not_null = !!a ? *a : !!b ? *b : !!c ? *c : *d;
  return x + not_null * 3 / 2 ;
}

int h1(int x, int not_null)
{
  return x + not_null * 3 / 2 ;
}

Ты реально ненавидишь паттерн-матчинг.

switch (a, b, c, d) {
case NULL, NULL, NULL, NULL:
        break;
case true, true, true, true:
        break;
case _, _, _, _:
        break;
}

Заметь, что в одной ветке используется NULL, а в другой true - значение указателя преобразуется к логическому, как и положено в Си. Если тебе не нравится идея преобразования:

switch (a != NULL, b != NULL, c != NULL, d != NULL) {
case true, true, true, true:
        break;
case false, false, false, false:
        break;
case _, _, _, _:
        break;
}

вариантов должно быть 5, и точка

я щас перепишу с твоим подходом

> вариантов должно быть 5, и точка

Ну, если нужно _всё в точности_ как у тебя, и напиши так, как сам написал, в чем проблема? То, что ты изначально написал - тоже примитивный паттерн-матчинг, кстати.

Ты реально ненавидишь паттерн-матчинг.

возможно, я не умею его готовить :-)

int h( maybe<int> a,  maybe<int> b,  maybe<int> c,  maybe<int> d)
{
  int x = g();

  switch( a; b; c; d ) {
    case Nothing; Nothing; Nothing; Nothing : return x;
    case Just(aa); Nothing; Nothing; Nothing :
    case Nothing; Just(aa); Nothing; Nothing :
    case Nothing; Nothing; Just(aa); Nothing :
    case Nothing; Nothing; Nothing; Just(aa) : return h1(x, aa);
    case Just(aa); Just(bb); Nothing; Nothing :
    case Just(aa); Nothing; Just(bb); Nothing :
    case Just(aa); Nothing; Nothing; Just(bb) :
    case Nothing; Just(aa); Just(bb); Nothing :
    case Nothing; Just(aa); Nothing; Just(bb) :
    case Nothing; Nothing; Just(aa); Just(bb) : return h2(x, aa, bb);
    /* тут мне лень было выписывать 4 варианта правильно*/
    case Just(aa); Nothing; Nothing; Nothing :
    case Nothing; Just(aa); Nothing; Nothing :
    case Nothing; Nothing; Just(aa); Nothing :
    case Nothing; Nothing; Nothing; Just(aa) : return h3(x, aa, bb, cc);
    case Just(aa); Just(bb); Just(cc); Just(dd) : return x+aa+bb+cc+dd;
}

> Ну, если нужно _всё в точности_ как у тебя, и напиши так, как сам написал, в чем проблема? То, что ты изначально написал - тоже примитивный паттерн-матчинг, кстати.

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

> switch (a, b, c, d)

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

>> Ты реально ненавидишь паттерн-матчинг.

возможно, я не умею его готовить :-)

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

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

int h( maybe<int> a,  maybe<int> b,  maybe<int> c,  maybe<int> d)
{
  int x = g(),

  switch( a, b, c, d ) {
    case (Nothing, Nothing, Nothing, Nothing) : return x;
    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);
    case (Just(aa), Just(bb), Nothing, Nothing),
         (Just(aa), Nothing, Just(bb), Nothing),
         (Just(aa), Nothing, Nothing, Just(bb)),
         (Nothing, Just(aa), Just(bb), Nothing),
         (Nothing, Just(aa), Nothing, Just(bb)),
         (Nothing, Nothing, Just(aa), Just(bb)): return h2(x, aa, bb);
    case (Nothing, Just(aa), Just(bb), Just(cc)),
         (Just(aa), Nothing, Just(bb), Just(cc)),
         (Just(aa), Just(bb), Nothing, Just(cc)),
         (Just(aa), Just(bb), Just(cc), Nothing): return h3(x, aa, bb, cc);
    case (Just(aa), Just(bb), Just(cc), Just(dd)): return x+aa+bb+cc+dd;
}

есть ли вариант лучше?

> Ты его именно ненавидишь. Иначе я никак не могу объяснить, что вместо того, чтобы матчить сумму ряда признаков, ты матчишь весь ряд - при том, что для тебя имеет смысл только агрегированное значение.

непонимаю — я же с самого начала сделал свитч по сумме

напиши свой вариант в любом синтаксисе, только чтобы в нем вызывались h1, h2, h3

> я же с самого начала сделал свитч по сумме

Видимо, ты не считаешь switch паттерн-матчингом.

напиши свой вариант в любом синтаксисе, только чтобы в нем вызывались h1, h2, h3

Зачем? Пойнт в том, что если тебе нужно матчить сумму - так и делай. И получишь свой изначальный switch, но в синтаксической обертке какого-нибудь паттерн-матчинга.

> И получишь свой изначальный switch, но в синтаксической обертке какого-нибудь паттерн-матчинга.

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

>> я же с самого начала сделал свитч по сумме

Видимо, ты не считаешь switch паттерн-матчингом.

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

бласт такое (ну или аналогичное) умеет, а вот то, что обычно называют паттерн-матчингом — похоже что не умеет

match one_if_notnull(a) + one_if_notnull(b) + one_if_notnull(c) + one_if_notnull(d) with
0 -> (* whatever *);
1 -> (* whatever *);
2 -> (* whatever *);
3 -> (* whatever *);
end

Функцию one_if_notnull, я надеюсь, писать не нужно? В Си ты ее использовал в виде !!.

Видимо, ты не считаешь switch паттерн-матчингом.

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

...только своей примитивностью

тем, что на первый взгляд строка case 4: ... кажется разыменовывающей нулевые указатели, а после анализа — не кажется

Паттерн матчинг здесь не причем.

>мы, как я понимаю, не можем, т.к. x +. a +. b +. c +. d будет типа MayBe Int, так?

scala> val l = Some(1) :: None :: Some(2) :: Nil;
l: List[Option[Int]] = List(Some(1), None, Some(2))

scala> l.flatMap(x=>x).foldLeft(0)(_ + _);
res1: Int = 3

подключайся

там проблема вовсе не в том, чтобы просуммировать Option-альные значения