Подтвердить что ты не робот

Статические типы, полиморфизм и специализация

Когда я впервые узнал Haskell, я очень быстро полюбил параметрический полиморфизм. Это восхитительно простая идея, которая работает удивительно хорошо. Целый "если он компилирует его, как правило, работает правильно", в основном из-за параметрического полиморфизма, ИМХО.

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

Это, в некотором смысле, немного похоже на шаблоны С++. Полиморфизм во время выполнения не существует, а только полиморфизм времени компиляции. Компилятор Haskell мог бы генерировать отдельный машинный код для каждого типа, в котором вызывается каждая полиморфная функция. Большинство компиляторов Haskell этого не делают, но вы можете реализовать его, если хотите.

Только если вы начнете добавлять расширения Haskell (ExistentialQuantification является очевидным), вы начинаете получать реальный полиморфизм во время выполнения, где у вас есть значения, тип которых не может быть статически вычислен.

О, да, мой вопрос?

  • Правильны ли правильные выражения?

  • Существует ли широко используемое имя для этого свойства?

4b9b3361

ОТВЕТЫ

Ответ 1

Haskell (без расширений) допускает полиморфную рекурсию, и эта особенность сама по себе не позволяет статически специализировать программу на полностью мономорфную. Вот программа, которая будет печатать N-глубокий вложенный список, где N - параметр командной строки:

import System

foo :: Show a => Int -> a -> IO ()
foo 0 x = print x
foo n x = foo (n-1) [x]

main = do [num_lists] <- getArgs
          foo (read num_lists) 0

В первом вызове foo, a имеет тип Int. В следующем рекурсивном вызове он имеет тип [Int], затем [[Int]] и т.д.

Если полиморфная рекурсия запрещена, то я считаю возможным статически специализировать программу.

Ответ 2

Да, я тоже об этом подумал. В принципе, идея состоит в том, что кажется, что вы можете реализовать Haskell 98, но не некоторые расширения языка для него, используя полиморфизм по-мультиинстантированию вместо полиморфизма по боксу.

Вы можете получить некоторое представление об этом, пытаясь реализовать некоторые функции Haskell в виде библиотек С++ (как вы заметили, С++ делает полиморфизм по-мультиинстационализации). Вы обнаружите, что можете делать все, что может сделать Haskell, за исключением того, что невозможно иметь полиморфные значения, которые включают ссылки на полиморфные функции.

Похоже, что если у вас

template<typename T>
void f(T);           // f :: a -> IO ()

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

&f<int>

но вы не можете взять адрес шаблона (&f). Это имеет смысл: шаблоны являются чисто компиляцией. Также имеет смысл, что если вы выполняете полиморфизм посредством многопоточности, у вас может быть указатель на какой-либо конкретный экземпляр, но вы не можете иметь указатель на полиморфную функцию, потому что на уровне машинного кода ее нет.

Итак, где Haskell использует полиморфные значения? На первый взгляд кажется, что хорошим правилом является "везде, где вам нужно писать явный forall". Итак, PolymorphicComponents, Rank2Types, RankNTypes и ImpredicativeTypes очевидны no-nos. Вы не можете перевести это на С++:

data MkList = MkList (forall a. a -> [a])
singleton = MkList (\x -> [x])

С другой стороны, ExistentialQuantification выполнимо, по крайней мере, в некоторых случаях: это означает, что у него есть неклассический класс с конструктором шаблона (или, более общо, класс, конструктор которого построен на большинстве вещей, чем сам класс).

Если в Haskell у вас есть:

data SomeShow = forall a. Show a => SomeShow a
instance Show SomeShow where show (SomeShow a) = show a

вы можете реализовать это в С++ как:

// a function which takes a void*, casts it to the given type, and
// calls the appropriate show() function (statically selected based
// on overload resolution rules)
template<typename T>
String showVoid(void *x)
{
    show(*(T*)x);
}

class SomeShow
{
    private:
        void *m_data;
        String (*m_show)(void*); // m_show :: Any -> String

    public:
        template<typename T>
        SomeShow(T x)
            : m_data(new T(x)) // memory management issues here, but that orthogonal
            , m_show(&showVoid<T>)
        {
        }

        String show()
        {
            // alternately we could declare the top-level show() as a friend and
            // put this there
            return m_show(m_data);
        }
};

// C++ doesn't have type classes per se, but it has overloading, which means
// that interfaces are implicit: where in Haskell you would write a class and
// instances, in C++ you just write a function with the same name for each type
String show(SomeShow x)
{
    return x.show();
}

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

Итак, мы показали, что есть некоторые расширения языка, которые вы можете реализовать, а некоторые из них не могут, но как насчет другой стороны монеты: есть ли что-нибудь в Haskell 98, которое вы не можете реализовать? Судя по тому, что вам нужно расширение языка (ExplicitForAll), чтобы даже написать forall, вы бы подумали, что ответ отрицательный. И вы почти правы, но есть две морщины: классы типов и полиморфная рекурсия. Классы типов обычно реализуются с использованием передачи словаря: каждое объявление экземпляра приводит к записи функций, которые неявно передаются туда, где они нужны.

Итак, для Монады, например, у вас будет:

data MonadDict m = MonadDict { 
    return :: forall a. a -> m a,
    (>>=)  :: forall a b. m a -> (a -> m b) -> m b
}

Хорошо бы вы посмотрели на эти фолк! Вы не можете писать их явно, но в реализациях пересылки словаря, даже в Haskell 98, классы с полиморфными методами приводят к записи, содержащие полиморфные функции. Что, если вы пытаетесь реализовать все это, используя multiinstantion, очевидно, будет проблемой. Вы можете почти уйти без прохождения словаря, потому что, если вы придерживаетесь Haskell 98, экземпляры почти всегда глобальны и статически известны. Каждый экземпляр приводит к некоторым полиморфным функциям, но из-за того, что вызов для вызова почти всегда известен во время компиляции, вам почти никогда не нужно передавать ссылки на них во время выполнения (что хорошо, потому что вы не можете). Компромисс заключается в том, что вам нужно делать компиляцию всей программы, потому что в противном случае экземпляры больше не статически известны: они могут быть в другом модуле. И исключением является полиморфная рекурсия, которая практически требует от вас создания словаря во время выполнения. Дополнительную информацию об этом см. В другом ответе. Полиморфная рекурсия убивает многопотоковый подход даже без классов типов: см. Комментарий о BTree s. (Также классы ExistentialQuantification * plus * с полиморфными методами больше не выполняются, потому что вам придется снова начать хранить указатели для полиморфных функций.)

Ответ 3

Целые компиляторы программ используют глобальный доступ к информации о типе, чтобы сделать очень агрессивную оптимизацию, как вы описали выше. Примеры включают JHC и MLton. GHC с inlining также частично "целая программа", по аналогичным причинам. Другие методы, которые используют глобальную информацию, включают суперкомпилирование.

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