LINUX.ORG.RU

Haskell vs. C++ : поддержка зависимых типов


0

0

Дискуссия началась при обсуждении Хаскеля 2010

Мой тезис состоит в том, что в Хаскеле поддержка зависимых типов хуже, чем в с++. (А как дело обстоит с Template Haskell?)

И пока что Miguel не представил определение зависимых типов (или ссылку на нее), по которому можно однозначно рассудить, есть ли в с++ зависимые типы. Боюсь, что пока я не реализую ему на шаблонах всю agda, он не согласится на наличие зависимых типов в с++ :-)

В процессе обсуждение родилось задание, похожее вот на это:

создаем вектор a с размерностью вводимой юзером

создаем вектор b с размерностью вводимой юзером

попытка перемножить несовместимые вектора a*b не компилируется

создаем вектор с с размерностью, равной размерности вектора а

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

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

Вот как я это сделал:

/*

$ g++ -DTRY dependent-type5.cxx
dependent-type5.cxx: In function ‘int main()’:
dependent-type5.cxx:68: error: no match for ‘operator*’ in ‘a * b’
dependent-type5.cxx:35: note: candidates are: double Vector<dimension>::operator*(const Vector<dimension>&) [with unsigned int* dimension = (& x)]
$ g++ dependent-type5.cxx
$ ./a.out
please enter dimension for vector a: 2
please enter element #0 for vector a: 1
please enter element #1 for vector a: 2
please enter dimension for vector b: 1
please enter element #0 for vector b: 1
please enter element #0 for vector c: 1
please enter element #1 for vector c: 2
a*c = 5
please enter element #0 for vector d: 1
please enter element #1 for vector d: 2
f(a)= 5

*/
#include <iostream>
#include <vector>

template<unsigned int* dimension> class Vector
{
  public:
    Vector(const char* msg): v( *dimension = *dimension ? *dimension : get_dimension(msg) ), dim(dimension)
    {
      for(int i=0; i<*dimension; i++) {
        std::cout << "please enter element #" << i << " for vector " << msg << ": ";
        std::cin >> v[i];
      }
    }
    double operator* (const Vector<dimension>& that) /// вот тут мы следим за размерностью! зависимые типы, да.
    {
      double result=0;
      for(int i=0; i<*dimension; i++)
        result += v[i] * that.v[i];
      return result;
    }
  private:
    std::vector<double> v;
    const unsigned int* const dim; /// для полноты картины

    static unsigned int get_dimension(const char* msg)
    {
      unsigned int result;
      std::cout << "please enter dimension for vector " << msg << ": ";
      std::cin >> result;
      return result;
    }
};

template<unsigned int* dimension> double f(Vector<dimension> a)
{
  Vector<dimension> d("d");
  return a*d;
}

unsigned int x=0, y=0;

int main()
{
  Vector<&x> a("a");                     /// создаем вектор a с размерностью вводимой юзером
  Vector<&y> b("b");                     /// создаем вектор b с размерностью вводимой юзером
#ifdef TRY
  double z0 = a*b;                       /// попытка перемножить несовместимые вектора a*b не компилируется
#endif
  Vector<&x> c("c");                     /// создаем вектор с с размерностью, равной размерности вектора а
                                         /// (это можно записать по-другому: typeof(a) c("c"); но вероятно это не нужно)
                                         /// (однако если все же нужно, потребуется с++0х)
  double z1 = a*c;                       /// попытка перемножить совместимые вектора a*с компилируется
  std::cout << "a*c = " << z1 << "\n";   /// выводим результат -- скалярное произведение
  double z2 = f(a);                      /// теперь считаем то же самое, но как вызов функции f -- компилируется
                                         /// (важно то, что размерность в явном виде в функцию f не передается) 
  std::cout << "f(a)= " << z2 << "\n";   /// снова выводим результат -- скалярное произведение

  return 0;
}

Комментарий: если размерность, поданная вектору, нулевая, он ее читает от юзера, а если ненулевая — то использует.

(Кто знает Qi? интересно было бы взглянуть на решение на нем)

Решение на Template Haskell с UnsafeIO наверно подойдет, но интересно было бы попугать народ полноценным решением без UnsafeIO :-)

И еще меня интересуе, как переписать на (Template?) Haskell вот это (даже если тут нет зависимых типов):

const int n=17;

...

Z<n> f(int x) { return mod<n>(x+(n/2)); }

Haskell vs. C++ : поддержка зависимых типов

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

www_linux_org_ru ★★★★★ ()

Haskell vs. C++ : поддержка зависимых типов

Так при чем здесь зависимые типы? Это даже не сработает при локальных нестатичных x и y. Точно такого же эффекта можно было добиться, используя обыкновенный ptrdiff_t в качестве параметра, который задавал бы смещение в глобальном массиве. Но это же не зависимые типы. Ты и сам это прекрасно понимаешь.

P.S. После просмотра этого кода дико хочется водки.

balodja ★★★ ()

Haskell vs. C++ : поддержка зависимых типов

Nice try, но...

Никаких статических гарантий это, конечно, не даёт (да ещё и не падает при их нарушении). Достаточно сказать сразу после #endif-а [code] x=0 [/code] и мы сразу их увидим. Я бы советовал сделать dimension приватным статическим членом класса, а не параметром шаблона.

Но настоящая проблема даже не в этом. По сути, здесь понятие равенства по значению подменяется понятием равенства по ссылке. То есть, простейшее [code] if (x == y) { cout << x*y } else { cout << 0 } [/code] тоже не скомпилится. И никакими ухищрениями заставить его скомпилиться невозможно. То есть, фактически, просто заводятся два разных типа VectorA и VectorB, и значения одного типа никак не соотносятся со значениями другого. Никакого отношения к зависимым типам оно, конечно, не имеет. В зависимых типах ТИП одной переменной зависит от ЗНАЧЕНИЯ другой. Значения, а не расположения в памяти.

const int n=17;

Z<n> f(int x) { return mod<n>(x+(n/2)); }

Простейший вариант type-level-арифметики (поэтому будет немножко длинно): [code] data Z = Zero newtype S a = Succ a class Pointed a where point :: a instance Pointed Z where point = Zero instance Pointed a => Pointed (S a) where point = Succ point class Value a where value :: a -> Integer instance Value Z where value Zero = 0 instance Value a => Value (S a) where value (Succ x) = 1 + value x [/code] Написанное выше, естественно, пишется один раз. [code] type N = S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))) f :: Value a => a -> Integer -> Integer f n x = let v = value n in (x + v `div` 2) `mod` v main = print $ f (point :: N) 239 [/code]

Miguel ★★★★★ ()

Haskell vs. C++ : поддержка зависимых типов

РРРРРРР!!!!

Nice try, но...

Никаких статических гарантий это, конечно, не даёт (да ещё и не падает при их нарушении). Достаточно сказать сразу после #endif-а

x=0
и мы сразу их увидим. Я бы советовал сделать dimension приватным статическим членом класса, а не параметром шаблона.

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

if (x == y) {
  cout << x*yж
} else {
  cout << 0ж
}
тоже не скомпилится. И никакими ухищрениями заставить его скомпилиться невозможно. То есть, фактически, просто заводятся два разных типа VectorA и VectorB, и значения одного типа никак не соотносятся со значениями другого. Никакого отношения к зависимым типам оно, конечно, не имеет. В зависимых типах ТИП одной переменной зависит от ЗНАЧЕНИЯ другой. Значения, а не расположения в памяти.

↑ > const int n=17;

↑ > Z<n> f(int x) { return mod<n>(x+(n/2)); }

↑ Простейший вариант type-level-арифметики (поэтому будет немножко длинно):

data Z = Zero
newtype S a = Succ a
class Pointed a where point :: a
instance Pointed Z where point = Zero
instance Pointed a => Pointed (S a) where point = Succ point
class Value a where value :: a -> Integer
instance Value Z where value Zero = 0
instance Value a => Value (S a) where value (Succ x) = 1 + value x 
Написанное выше, естественно, пишется один раз.
type N = S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))
f :: Value a => a -> Integer -> Integer
f n x = let v = value n in (x + v `div` 2) `mod` v
main = print $ f (point :: N) 239

Miguel ★★★★★ ()
Ответ на: Haskell vs. C++ : поддержка зависимых типов от Miguel

Haskell vs. C++ : поддержка зависимых типов

> Никаких статических гарантий это, конечно, не даёт (да ещё и не падает при их нарушении). Достаточно сказать сразу после #endif-а [code] x=0 [/code] и мы сразу их увидим.

я тебя не до конца понял...

х=0 говорить в общем-то нельзя, но для формализации этого придется потратить еще n строчек кода, от которого отдельным гражданам уже хочется водки :-) возможно таки придется потратить

www_linux_org_ru ★★★★★ ()
Ответ на: Haskell vs. C++ : поддержка зависимых типов от balodja

Haskell vs. C++ : поддержка зависимых типов

> Так при чем здесь зависимые типы? Это даже не сработает при локальных нестатичных x и y. Точно такого же эффекта можно было добиться, используя обыкновенный ptrdiff_t в качестве параметра, который задавал бы смещение в глобальном массиве.

Но это же не зависимые типы. Ты и сам это прекрасно понимаешь.

Определение в студию. Чтобы не размазня и сопли как в википедии, и не «сам понимаешь», а была возможна проверка.

www_linux_org_ru ★★★★★ ()
Ответ на: Haskell vs. C++ : поддержка зависимых типов от balodja

Haskell vs. C++ : поддержка зависимых типов

> Это даже не сработает при локальных нестатичных x и y.

и не должно, x и y выбраны специально статичными

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

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

www_linux_org_ru ★★★★★ ()
Ответ на: Haskell vs. C++ : поддержка зависимых типов от www_linux_org_ru

Haskell vs. C++ : поддержка зависимых типов

> Чтобы не размазня и сопли как в википедии, и не «сам понимаешь», а была возможна проверка.

Я тебе уже сказал, могу разъяснить чуть подробнее. Переменная A, тип которой зависит от ЗНАЧЕНИЯ переменной B. Именно значения, и именно переменной - то есть, от того, что во время компиляции неизвестно. При этом должна сохраняться проверка типов во время компиляции. Да, и: зависимость (типа от значения) должна быть, разумеется, функциональной - т.е., если значения равны, то и типы равны.

Так что Vector<x> и Vector<y> можно, например, перемножать, если мы в состоянии статически гарантировать, что x==y. Например (хотя это не единственный вариант) сделав это внутри if (x==y).

Miguel ★★★★★ ()
Ответ на: Haskell vs. C++ : поддержка зависимых типов от Miguel

Haskell vs. C++ : поддержка зависимых типов

> Так что Vector<x> и Vector<y> можно, например, перемножать, если мы в состоянии статически гарантировать, что x==y. Например (хотя это не единственный вариант) сделав это внутри if (x==y).

мы в состоянии статически гарантировать что x==y например в том случае, если &x==&y, что у меня и проверяется

если же тебе надо написать *именно* if (x==y) вместо if (&x==&y), то это можно сделать

www_linux_org_ru ★★★★★ ()
Ответ на: Haskell vs. C++ : поддержка зависимых типов от Miguel

Haskell vs. C++ : поддержка зависимых типов

но понятно, что может быть всегда x==y, а компилятор не настолько умен, чтобы это доказать; и более того — это скорее общий случай. об этом я и талдычу.

www_linux_org_ru ★★★★★ ()
Ответ на: Haskell vs. C++ : поддержка зависимых типов от Miguel

Haskell vs. C++ : поддержка зависимых типов

* если же тебе надо написать *именно* if (x==y) вместо if (&x==&y), то это можно сделать, но семантика останется прежняя — равенство указателей

я повторю — ты провел границу зависимых типов произвольно!

так или иначе компилятор столкнется со случаями, когда не сможет статически что-то доказать, и у меня это происходит рано (когда &x!=&y), а в другой системе произойдет, позже, но произойдет — и совершенно безосновательно ты один случай считаешь зависимыми типами, а другой — нет.

www_linux_org_ru ★★★★★ ()
Ответ на: Haskell vs. C++ : поддержка зависимых типов от Miguel

Haskell vs. C++ : поддержка зависимых типов

Я имел в виду, конечно, if (x == y) {cout << a*b;} else {cout << 0;}

Давай рассмотрим такой код:

if( p(x,y) ) {cout << a*b;} else {cout << 0;}

предположим, что p(x,y) — достаточно сложно определенный предикат, который, однако, эквивалентен предикату x==y, однако доказательство эквивалентности требует доказать теорему ферма о разложении простого числа 4а+1 на сумму 2 квадратов

практически: 1. компилятор это не сможет 2. никто возится не будет, и разницы между моим случаем (не сумели доказать x==y, т.к. &x!=&y и на том весь разум исчерпан) нет

_________________________________________________________

так как все же на хаскеле написать аналог, который хотя бы умеет доказывать через (&x==&y) => (x==y) ?

www_linux_org_ru ★★★★★ ()
Ответ на: Haskell vs. C++ : поддержка зависимых типов от www_linux_org_ru

Haskell vs. C++ : поддержка зависимых типов

* однако доказательство эквивалентности требует доказать теорему ферма о разложении простого числа вида 4n+1 на сумму 2 квадратов

там «а» не связаны.

www_linux_org_ru ★★★★★ ()
Ответ на: Haskell vs. C++ : поддержка зависимых типов от www_linux_org_ru

Re: Haskell vs. C++ : поддержка зависимых типов

>так или иначе компилятор столкнется со случаями, когда не сможет статически что-то доказать, и у меня это происходит рано (когда &x!=&y), а

а в системе с зависимыми типами программа не скомпилируется.

anonymous ()
Ответ на: Re: Haskell vs. C++ : поддержка зависимых типов от anonymous

Haskell vs. C++ : поддержка зависимых типов

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

и у меня не скомпилируется.

разница с более серьезными системами в том, что у меня для логического вывода доступна только аксиома (&x==&y)=>(x==y), а в более серьезных — больше аксиом.

www_linux_org_ru ★★★★★ ()
Ответ на: Haskell vs. C++ : поддержка зависимых типов от www_linux_org_ru

Re: Haskell vs. C++ : поддержка зависимых типов

> так как все же на хаскеле написать аналог, который хотя бы умеет доказывать через (&x==&y) => (x==y) ?

А что такое «(&x==&y) => (x==y)»?

anonymous ()
Ответ на: Haskell vs. C++ : поддержка зависимых типов от www_linux_org_ru

Haskell vs. C++ : поддержка зависимых типов

> мы в состоянии статически гарантировать что x==y например в том случае, если &x==&y, что у меня и проверяется

Не например.

Успокойся. В темплейтах аргументами ВСЕГДА являются константы времени компиляции; зависимые типы требуют именно зависимости от РАНТАЙМОВОГО значения, на момент компиляции неизвестного. Темплейты просто НЕ МОГУТ помочь. Ничем.

Miguel ★★★★★ ()
Ответ на: Haskell vs. C++ : поддержка зависимых типов от www_linux_org_ru

Haskell vs. C++ : поддержка зависимых типов

> но понятно, что может быть всегда x==y, а компилятор не настолько умен, чтобы это доказать; и более того — это скорее общий случай. об этом я и талдычу.

Да компилятор ВООБЩЕ не в состоянии доказывать подобные вещи, если их истинность определяется в рантайме. Об этом я и талдычу.

Miguel ★★★★★ ()
Ответ на: Haskell vs. C++ : поддержка зависимых типов от www_linux_org_ru

Haskell vs. C++ : поддержка зависимых типов

> я повторю — ты провел границу зависимых типов произвольно!

Это не я. Это стандартное понимание. Если тебе угодно понимать под зависимыми типами что-то своё - твоё право, но спорить тогда вообще не о чем.

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

Здрасьте, а я на что?

Все системы, допускающие зависимые типы, дают достаточно средств для того, чтобы ПРОГРАММИСТ предъявил доказательство достаточно произвольного факта - как, например, равенство двух значений.

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

Miguel ★★★★★ ()
Ответ на: Haskell vs. C++ : поддержка зависимых типов от www_linux_org_ru

Haskell vs. C++ : поддержка зависимых типов

> так как все же на хаскеле написать аналог, который хотя бы умеет доказывать через [code] newtype VectorA = VectorA [Float] newtype VectorB = VectorB [Float] [/code] Ничего больше в твоём коде не содержится.

Miguel ★★★★★ ()
Ответ на: Haskell vs. C++ : поддержка зависимых типов от Miguel

Haskell vs. C++ : поддержка зависимых типов

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

newtype VectorA = VectorA [Float]
newtype VectorB = VectorB [Float]

Ничего больше в твоём коде не содержится.

Miguel ★★★★★ ()
Ответ на: Haskell vs. C++ : поддержка зависимых типов от www_linux_org_ru

Haskell vs. C++ : поддержка зависимых типов

> никто возится не будет

Почему же. На практике необходимость доказывать теорему Ферма не возникает никогда, а более простые случаи народ доказывать берётся. И потом, есть же всякие способы упрощать процесс доказательства - скажем, «тактики» из Coq-а.

Miguel ★★★★★ ()

Haskell vs. C++ : поддержка зависимых типов

> создаем вектор a с размерностью вводимой юзером

создаем вектор b с размерностью вводимой юзером

попытка перемножить несовместимые вектора a*b не компилируется

Для того, чтоб пользователю ввести размерность вектора - программу нужно скомпилировать. Как она может не компилироваться, если она уже скомпилированна?

anonymous ()
Ответ на: Haskell vs. C++ : поддержка зависимых типов от anonymous

Haskell vs. C++ : поддержка зависимых типов

> Для того, чтоб пользователю ввести размерность вектора - программу нужно скомпилировать. Как она может не компилироваться, если она уже скомпилированна?

Ещё раз: если в программе возникает ситуация, когда мы можем гарантировать, что введены равные числа (например, внутри if-а), то операция перемножения должна быть допустима.

Miguel ★★★★★ ()
Ответ на: Haskell vs. C++ : поддержка зависимых типов от Miguel

Re: Haskell vs. C++ : поддержка зависимых типов

> Ещё раз: если в программе возникает ситуация, когда мы можем гарантировать, что введены равные числа (например, внутри if-а), то операция перемножения должна быть допустима.

Допустима - это не выкидывать abort()/sigfpe?

anonymous ()

Haskell vs. C++ : поддержка зависимых типов

Запарил уже ЛОР на ЛОРе.

l5k ()
Ответ на: Haskell vs. C++ : поддержка зависимых типов от Miguel

Re: Haskell vs. C++ : поддержка зависимых типов

> Ещё раз: если в программе возникает ситуация, когда мы можем гарантировать, что введены равные числа (например, внутри if-а), то операция перемножения должна быть допустима.

Как-то странно. А не логичнее было бы, что в случае «малейшей» возможности в разности размерностей программа падала на тайп-чекинге?

anonymous ()
Ответ на: Re: Haskell vs. C++ : поддержка зависимых типов от anonymous

Haskell vs. C++ : поддержка зависимых типов

> А не логичнее было бы, что в случае «малейшей» возможности в разности размерностей программа падала на тайп-чекинге?

Разумеется. Но если мы (например!) находимся в первой ветке if (x==y), то нет даже малейшей возможности. Именно такие вещи позволяют отслеживать зависимые типы.

Miguel ★★★★★ ()
Ответ на: Haskell vs. C++ : поддержка зависимых типов от Miguel

Re: Haskell vs. C++ : поддержка зависимых типов

> Но если мы (например!) находимся в первой ветке if (x==y), то нет даже малейшей возможности.

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

anonymous ()
Ответ на: Re: Haskell vs. C++ : поддержка зависимых типов от anonymous

Haskell vs. C++ : поддержка зависимых типов

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

Нет, почему же. Просто, если написано

if (x == y) {
  cout << a*b;
} else {
  cout << 0;
}
то компилятор должен это пропускать, а если
if (x == y) {
  cout << 0;
} else {
  cout << a*b;
}
то, соответственно, не пропускать. На этапе компиляции.

Разумеется, могут быть более сложные ситуации, как и говорил топикстартер. В этом случае так: если программист предоставил доказательство того, что в некоторой ветке программы x==y, то в этой ветке использовать a*b можно. И, само собой, недостаточно просто заявлений «а у нас доказательство того, что x==y возможно только если &x==&y, причём обе переменные - статические», нужно иметь возможность рассуждать о значениях переменных, а не об адресах.

Miguel ★★★★★ ()
Ответ на: Haskell vs. C++ : поддержка зависимых типов от Miguel

Re: Haskell vs. C++ : поддержка зависимых типов

> как и говорил топикстартер.

Топи-стартер попробовал скрестить ежа и ужа, но у него получился котопёс. Вот он, С++ головного мозга.

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

anonymous ()
Ответ на: Haskell vs. C++ : поддержка зависимых типов от Miguel

> Нет, почему же. Просто, если написано ... то компилятор должен это пропускать, а если ... то, соответственно, не пропускать. На этапе компиляции.

В этом есть практический смысл.

Ладно, подумаю насчет реализации if (правда он будет IF).

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

Лучше кинь несколько примеров, например (a~b~c)*(c~b~a) где ~ это операция конкатенации, * это скалярное произведение.

www_linux_org_ru ★★★★★ ()
Ответ на: Re: Haskell vs. C++ : поддержка зависимых типов от anonymous

> Топи-стартер попробовал скрестить ежа и ужа, но у него получился котопёс. Вот он, С++ головного мозга.

Хе-хе.

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

А дальше будет свой язык.

www_linux_org_ru ★★★★★ ()
Ответ на: комментарий от Miguel

> Так я же и твержу: нигде. Нету их, ни в плюсах, ни в Хаскеле.

через 2-3 дня я отпишусь, получился ли у меня IF, а пока можешь твердить

www_linux_org_ru ★★★★★ ()
Ответ на: комментарий от www_linux_org_ru

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

Ну вообще-то неплохо не забывать о том что данные для обработки в программу будут поступать *после* того как она будет скомпилирована, а не *до*. Поэтому непонятно зачем тут собственно нужна вся эта статика. А ошибки вида «прибавить вес к длине» ловят уже существующие языки типа Ады. Но, судя по истории с Арианом-5, тут есть ньюансы.

Absurd ★★★ ()
Ответ на: комментарий от Absurd

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

она нужна, т.к. например x+y+z==z+y+x, и мы можем написать (a~b~c)*(c~b~a), но не можем в общем случае например (a~b~c)*(a~b~b)

www_linux_org_ru ★★★★★ ()
Ответ на: Haskell vs. C++ : поддержка зависимых типов от Miguel

>зависимые типы требуют именно зависимости от РАНТАЙМОВОГО значения, на момент компиляции неизвестного.
Это ересь. Можно пример системы с рантаймовой проверкой зависимых типов?
Проверка идет на стадии type check. Просто есть вычисления на типах.

Советую курнуть Барендрегта Lambda calcluli with types, доступен русский перевод на сайте http://spbhug.folding-maps.org/wiki/LambdaCube
А потом можно покурить на тему Coq (но это не ЯП вобщем-то), Epigram (ЯП, но неудобен и заброшен), Agda2 (хаскелистам - самое оно, но слегка академично, рекомендую именно это), ATS (окамлистам, но много очень марсианских фичей)

ratatosk ()
Ответ на: комментарий от ratatosk

p.s. насчет компайл-тайм проверок, стандартный экзампл для Agda - это mergesort, который ДОКАЗАННО сортирует. А вы тут про длимы векторов говорите, децкий сад :)

ratatosk ()
Ответ на: комментарий от ratatosk

И что, собственно, доказывается?

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

Love5an ()
Ответ на: комментарий от ratatosk

> Это ересь. Можно пример системы с рантаймовой проверкой зависимых типов?

Нельзя, типы проверяются на стадии компиляции.

Miguel ★★★★★ ()
Ответ на: комментарий от Love5an

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

Да это давно уже есть, шо в Лиспе, шо в C++, шо даже в Хаскеле (но не в Haskell98).

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

Разница очевидная, компилируем на машине разработчика, результат работает на машине пользователя.

Miguel ★★★★★ ()
Ответ на: комментарий от Miguel

>Разница очевидная, компилируем на машине разработчика, результат работает на машине пользователя.

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

Absurd ★★★ ()
Ответ на: комментарий от www_linux_org_ru

>мы можем написать (a~b~c)*(c~b~a), но не можем в общем случае например (a~b~c)*(a~b~b)

В общем случае мы не можем ничего. При вычислениях на плавающей запятой мы даже не можем утверждать что a+(b+c)=(a+b)+c.

Absurd ★★★ ()
Ответ на: комментарий от Miguel

>Нельзя, типы проверяются на стадии компиляции.
Значит я тебя неправильно понял.

ratatosk ()
Вы не можете добавлять комментарии в эту тему. Тема перемещена в архив.