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)); }

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

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

Опять!!!

Что бы ни вводил пользователь, внутри первой ветки ветвления if (x == y) можно достоверно утверждать, что x == y. Более того, можно достоверно утверждать, что 3x+2y = x+4y.

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

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

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

Я выражался предельно ясно - допустим ты при помощи статических проверок доказал что пре-кондишены для операции над матрицами соблюдены (размеры совпадают) и ты можешь их к примеру перемножить. Но при этом не понятно что делать в случае если они не соблюдены. Если тупо кидать экзепшен, то непонятно в чем тут профит.

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

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

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

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

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

Поэтому интересно, насколько непросто?

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

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

> Но при этом не понятно что делать в случае если они не соблюдены. Если тупо кидать экзепшен, то непонятно в чем тут профит.

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

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

>Вся остальная программа гарантированно корректна.

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

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

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

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

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

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

Доказать себе я могу, зачем доказывать компилятору?

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

> Неразрешимость задачи останова была доказана Тьюрингом.

«Ты ходил в школу, парень? Так почему ты там не остался?!» // У.Гибсон «Граф Ноль»

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

> Доказать себе я могу, зачем доказывать компилятору?

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

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

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

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

> Именно значения, и именно переменной - то есть, от того, что во время компиляции неизвестно. При этом должна сохраняться проверка типов во время компиляции.

Т.е. язык с зависимыми типами не может быть интерпретируемым?

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