Зависимые типы в Haskell: почему это будущее разработки программного обеспечения

Original author: Vladislav Zavialov
  • Translation


В Serokell мы занимаемся не только коммерческими проектами, но стараемся изменить мир к лучшему. Например, работаем над улучшением главного инструмента всех хаскелистов – Glasgow Haskell Compiler (GHC). Мы сосредоточились на расширении системы типов под впечатлением от работы Ричарда Айзенберга "Зависимые типы в Haskell: теория и практика".


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


Текущее положение дел


Алгоритм выбора языка программирования


Зависимые типы – это то, чего мне больше всего не хватает в Haskell. Давайте обсудим почему. От кода мы хотим:


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

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


Стандартный Haskell: эргономика + производительность


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


Языки с небезопасным доступом к памяти, такие как C, приводят к самым серьезным ошибкам и уязвимостям (например, переполнение буфера, утечки памяти). Иногда такие языки нужны, но чаще всего их применение – идея так себе.


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


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


Динамически типизированные (или, скорее, монотипизированные) языки, такие как JavaScript или Clojure, не предоставляют статический анализ, а следовательно не могут обеспечить тот же уровень уверенности в правильности кода (и нет, тесты не могут заменить типы – нужно и то, и другое!).


Статически типизированные языки, такие как Java или Go, часто имеют сильно ограниченную систему типов. Это вынуждает программистов писать избыточный код и пускать в дело небезопасные возможности языка. Например, отсутствие обобщенных типов в Go вынуждает использовать interface{} и приведение типов времени выполнения. Также нет разделения между вычислениями с побочными эффектами (ввод, вывод) и чистыми вычислениями.


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


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


В качестве простого примера того, где система типов Haskell недостаточно мощна, рассмотрим оператор индексирования списка из Prelude (или индексирование массива из пакета primitive):


(!!) :: [a] -> Int -> a
indexArray :: Array a -> Int -> a

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


Agda: эргономика + корректность


Средства доказательства теорем (например, Coq) — программные инструменты, которые позволяют с помощью компьютера разрабатывать формальные доказательства математических теорем. Для математика использование таких средств похоже на написание доказательств на бумаге. Различие в беспрецедентной строгости, требуемой компьютером, чтобы установить правильность такого доказательства.


Для программиста, однако, средство доказательства теорем не так уж отличается от компилятора для эзотерического языка программирования с невероятной системой типов (и, возможно, интегрированной средой разработки), и посредственным (или даже отсутствующим) всем остальным. Средство доказательства теорем – это, по сути, языки программирования, авторы которых все время потратили на разработку системы типизации и забыли, что программы еще надо запускать.


Заветная мечта разработчиков верифицированного программного обеспечения – это средство доказательства теорем, которое было бы хорошим языком программирования с высококачественными генератором кода и средой выполнения. В данном направлении экспериментировали в том числе создатели Idris. Но это язык со строгими (энергичными) вычислениями, а его реализация на данный момент не отличается стабильностью.


Среди всех средств доказательства теорем больше всего по душе хаскелистам Agda. Во многом она похожа на Haskell, но с более мощной системой типов. Мы в Serokell применяем её, чтобы доказывать различные свойства наших программ. Мой коллега Даня Рогозин написал серию статей об этом.


Вот тип функции lookup аналогичной оператору (!!) из Haskell:


lookup : ∀ (xs : List A) → Fin (length xs) → A

Первый параметр здесь имеет тип List A, который соответствует [a] в Haskell. Однако мы даем ему имя xs, чтобы обращаться к нему в оставшейся части сигнатуры типа. В Haskell мы можем обращаться к аргументам функции только в теле функции на уровне термов:


(!!) :: [a] -> Int -> a -- обращение к xs невозможно
(!!) = \xs i -> ...     -- обращение к xs возможно

А вот в Agda мы можем ссылаться на это значение xs и на уровне типов, что мы и делаем во втором параметре lookup, Fin (length xs). Функция, ссылающаяся на свой параметр на уровне типов, называется зависимой функцией и является примером зависимых типов.


Второй параметр в lookup имеет тип Fin n для n ~ length xs. Значение типа Fin n соответствует числу в диапазоне [0, n), так что Fin (length xs) это неотрицательное число меньше длины входного списка. Именно это нам и нужно, чтобы представить валидный индекс элемента списка. Грубо говоря, lookup ["x","y","z"] 2 проверку типов пройдет, а lookup ["x","y","z"] 42 не пройдет.


Когда дело доходит до запуска программ на Agda, мы можем скомпилировать их в Haskell с помощью бэкенда MAlonzo. Но производительность генерируемого кода будет неудовлетворительна. Это не вина MAlonzo: ему приходится вставлять многочисленные unsafeCoerce, чтобы GHC принимал код, уже проверенный Agda. Но тот же unsafeCoerce снижает производительность (по итогам обсуждения этой статьи выяснилось, что проблемы с производительностью возможно вызваны иными причинами – прим. автора).


Это ставит нас в затруднительное положение: нам приходится использовать Agda для моделирования и формальной проверки, а затем заново реализовывать ту же функциональность на Haskell. При такой организации рабочих процессов наш код на Agda выступает в качестве спецификации, проверяемой компьютером. Это лучше спецификации на естественном языке, но далеко от идеала. Цель – если код скомпилировался, то он будет работать в соответствии со спецификацией.


Haskell с расширениями: корректность + производительность



Стремясь к статическим гарантиям языков с зависимыми типами, GHC прошел долгий путь. В него добавляли расширения, увеличивающие выразительность системы типов. Я начал использовать Haskell, когда GHC 7.4 был новейшей версией компилятора. Уже тогда у него были основные расширения для продвинутого программирования на уровне типов: RankNTypes, GADTs, TypeFamilies, DataKinds, и PolyKinds.


И все же полноценных зависимых типов в Haskell нет до сих пор: ни зависимых функций (Π-типов), ни зависимых пар (Σ-типов). С другой стороны, хотя бы кодировка для них у нас есть!


Нынешние практики таковы:


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

Это приводит к значительному количеству избыточного кода, но библиотека singletons автоматизирует его генерацию посредством Template Haskell.



Так что самые смелые и решительные могут закодировать зависимые типы в Haskell уже сейчас. В качестве демонстрации вот реализация функции lookup аналогичная варианту на Agda:


{-# OPTIONS -Wall -Wno-unticked-promoted-constructors -Wno-missing-signatures #-}
{-# LANGUAGE LambdaCase, DataKinds, PolyKinds, TypeFamilies, GADTs,
             ScopedTypeVariables, EmptyCase, UndecidableInstances,
             TypeSynonymInstances, FlexibleInstances, TypeApplications,
             TemplateHaskell #-}

module ListLookup where

import Data.Singletons.TH
import Data.Singletons.Prelude

singletons
  [d|
    data N = Z | S N
    len :: [a] -> N
    len [] = Z
    len (_:xs) = S (len xs)
  |]

data Fin n where
  FZ :: Fin (S n)
  FS :: Fin n -> Fin (S n)

lookupS :: SingKind a => SList (xs :: [a]) -> Fin (Len xs) -> Demote a
lookupS SNil = \case{}
lookupS (SCons x xs) =
  \case
    FZ -> fromSing x
    FS i' -> lookupS xs i'

И вот сессия GHCi, показывающая, что lookupS действительно отклоняет слишком большие индексы:


GHCi, version 8.6.2: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling ListLookup       ( ListLookup.hs, interpreted )
Ok, one module loaded.
*ListLookup> :set -XTypeApplications -XDataKinds 
*ListLookup> lookupS (sing @["x", "y", "z"]) FZ
"x"
*ListLookup> lookupS (sing @["x", "y", "z"]) (FS FZ)
"y"
*ListLookup> lookupS (sing @["x", "y", "z"]) (FS (FS FZ))
"z"
*ListLookup> lookupS (sing @["x", "y", "z"]) (FS (FS (FS FZ)))

<interactive>:5:34: error:
    • Couldn't match type ''S n0' with ''Z'
      Expected type: Fin (Len '["x", "y", "z"])
        Actual type: Fin ('S ('S ('S ('S n0))))
    • In the second argument of 'lookupS', namely '(FS (FS (FS FZ)))'
      In the expression:
        lookupS (sing @["x", "y", "z"]) (FS (FS (FS FZ)))
      In an equation for 'it':
          it = lookupS (sing @["x", "y", "z"]) (FS (FS (FS FZ)))

Этот пример показывает, что осуществимое не означает практичное. Я рад, что в Haskell есть языковые возможности для реализации lookupS, но в то же время меня беспокоит возникающая при этом ненужная сложность. Вне исследовательских проектов такой стиль кода я бы не посоветовал.


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


Вот некоторые из них:


  • Отношение типизации a :: t и отношение назначения вида t :: k различны. 5 :: Integer верно в термах, но не в типах. "hi" :: Symbol верно в типах, но не в термах. Это приводит к необходимости семейства типов Demote для сопоставления видов и типов.
  • Стандартная библиотека использует Int в качестве представления списковых индексов (и singletons использует Nat в повышенных определениях). Int и Nat – неиндуктивные типы. Несмотря на большую эффективность по сравнению с унарным кодированием натуральных чисел, они не очень хорошо работают с индуктивными определениями, такими как Fin или lookupS. Из-за этого мы переопределяем length как len.
  • В Haskell нет встроенных механизмов повышения функций на уровень типов. singletons кодирует их в виде закрытых семейств типов и применяет дефункционализацию, чтобы обойти отсутствие частичного применения семейств типов. Эта кодировка сложна. Вдобавок, нам пришлось поместить определение len в цитату Template Haskell, чтобы singletons сгенерировал её аналог на уровне типов, Len.
  • Нет встроенных зависимых функций. Приходится использовать единичные типы, чтобы преодолеть разрыв между термами и типами. Вместо обычного списка мы передаем SList на вход lookupS. Поэтому мы должны держать в голове сразу несколько определений списков. Также это приводит к накладным расходам во время исполнения программы. Они возникают из-за конвертации между обычными значениями и значениями единичных типов (toSing, fromSing) и из-за передачи процедуры конвертации (ограничение SingKind).

Неудобство – это меньшая из проблем. Хуже то, что эти возможности языка работают ненадежно. Например, я сообщил о проблеме #12564 еще в 2016 году, а еще есть #12088 того же года. Обе проблемы препятствуют реализации программ более продвинутых, чем примеры из учебников (вроде индексирования списков). Эти баги GHC до сих пор не исправлены, и причина, как мне кажется, в том, что у разработчиков просто не хватает времени. Количество людей, активно работающих над GHC, удивительно мало, поэтому до некоторых вещей не доходят руки.


Резюме


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


Стандартный Haskell Agda Haskell с расширениями
Эргономика и поддерживаемость + + -
Производительность + - +
Корректность, гарантированная способом составления - + +

Светлое будущее


Из трех доступных вариантов каждый имеет свои недостатки. Тем не менее, мы можем их исправить:


  • Взять стандартный Haskell и добавить зависимые типы напрямую вместо неудобного кодирования через singletons. (Легче сказать, чем сделать).
  • Взять Agda и реализовать эффективный генератор кода и RTS для неё. (Легче сказать, чем сделать).
  • Взять Haskell с расширениями, исправить баги и продолжить добавлять новые расширения, чтобы упростить кодирование зависимых типов. (Легче сказать, чем сделать).

Хорошая новость в том, что все три варианта сходятся в одной точке (в каком-то смысле). Представьте себе самое минимальное расширение стандартного Haskell, которое добавляет зависимые типы, и следовательно, позволяет гарантировать корректность кода способом его составления. Код на Agda можно компилировать (транспилировать) в этот язык без unsafeCoerce. А Haskell с расширениями – это, в некотором смысле, незаконченный прототип этого языка. Что-то понадобится улучшить, а что-то убрать, но в конечном итоге, мы достигнем желаемого результата.


Избавление от singletons


Хорошим показателем прогресса можно считать упрощение библиотеки singletons. По мере реализации зависимых типов в Haskell, обходные пути и специальная обработка частных случаев, реализованные в singletons, становятся не нужны. В конечном итоге нужда в этом пакете пропадет полностью. Например, в 2016 году с помощью расширения -XTypeInType я убрал KProxy из SingKind и SomeSing. Это изменение стало возможным благодаря объединению типов и видов. Сравните старые и новые определения:


class (kparam ~ 'KProxy) => SingKind (kparam :: KProxy k) where
  type DemoteRep kparam :: *
  fromSing :: SingKind (a :: k) -> DemoteRep kparam
  toSing :: DemoteRep kparam -> SomeSing kparam

type Demote (a :: k) = DemoteRep ('KProxy :: KProxy k)

data SomeSing (kproxy :: KProxy k) where
  SomeSing :: Sing (a :: k) -> SomeSing ('KProxy :: KProxy k)

В старых определениях k встречается исключительно в позициях вида, справа от аннотаций вида t :: k. Мы используем kparam :: KProxy k для переноса k в типы.


class SingKind k where
  type DemoteRep k :: *
  fromSing :: SingKind (a :: k) -> DemoteRep k
  toSing :: DemoteRep k -> SomeSing k

type Demote (a :: k) = DemoteRep k

data SomeSing k where
  SomeSing :: Sing (a :: k) -> SomeSing k

В новых определениях k свободно перемещается между позициями вида и типа, так что нам больше не нужен KProxy. Причина в том, что начиная с GHC 8.0 типы и виды относятся к одной и той же синтаксической категории.


В стандартном Haskell есть три полностью разделенных мира: термы, типы и виды. Если посмотреть на исходный код GHC 7.10, то можно увидеть обособленный синтаксический анализатор для видов и обособленную проверку. В GHC 8.0 их больше нет: синтаксический анализатор и проверка для типов и видов общие.



В Haskell с расширениями вид – это всего лишь роль, в которой выступает тип:


f :: T z -> ...               -- 'z' это тип
g :: T (a :: z) -> ...        -- 'z' это вид
h :: T z -> T (a :: z) -> ... -- 'z' это и тип, и вид

В GHC 8.0–8.4 все еще оставались некоторые различия между разрешением имен в типах и видах. Но к GHC 8.6 я их свел к минимуму: создал расширение StarIsType и внес функциональность TypeInType в PolyKinds. Оставшиеся различия я сделал предупреждением к GHC 8.8, и полностью устранил в GHC 8.10 (перевод данного параграфа обновлен, в оригинале проделанные работы описываются как будущие задачи – прим. автора).


Каков следующий шаг? Давайте взглянем на SingKind в последней версии singletons:


class SingKind k where
  type Demote k = (r :: Type) | r -> k
  fromSing :: Sing (a :: k) -> Demote k
  toSing   :: Demote k -> SomeSing k

Семейство типов Demote необходимо для учета расхождений между отношением типизации a :: t и отношением назначения вида t :: k. Чаще всего (для алгебраических типов данных), Demote это тождественное отображение:


  • type Demote Bool = Bool
  • type Demote [a] = [Demote a]
  • type Demote (Either a b) = Either (Demote a) (Demote b)

Следовательно, Demote (Either [Bool] Bool) = Either [Bool] Bool. Это наблюдение побуждает нас сделать следующее упрощение:


class SingKind k where
  fromSing :: Sing (a :: k) -> k
  toSing   :: k -> SomeSing k

Demote не понадобился! И, в самом деле, это сработало бы как в случае Either [Bool] Bool, так и с другими алгебраическими типами данных. На практике, однако, мы имеем дело и с неалгебраическими типами данных: Integer, Natural, Char, Text, и так далее. Если их использовать в качестве видов, они не населены: 1 :: Natural верно на уровне термов, но не на уровне типов. Из-за этого мы имеем дело с такими определениями:


type Demote Nat = Natural
type Demote Symbol = Text

Решение этой проблемы в повышении примитивных типов. Например, Text определен так:


-- | A space efficient, packed, unboxed Unicode text type.
data Text = Text
    {-# UNPACK #-} !Array -- payload (Word16 elements)
    {-# UNPACK #-} !Int   -- offset (units of Word16, not Char)
    {-# UNPACK #-} !Int   -- length (units of Word16, not Char)

data Array = Array ByteArray#
data Int = I# Int#

Если мы как положено повысим ByteArray# и Int# на уровень типов, то сможем использовать Text вместо Symbol. Сделав то же самое с Natural и, возможно, парой других типов, можно избавиться от Demote, так ведь?


Увы, не так. В вышесказанном я закрыл глаза на самый главный тип данных: функции. У них тоже особый инстанс Demote:


type Demote (k1 ~> k2) = Demote k1 -> Demote k2

type a ~> b = TyFun a b -> Type
data TyFun :: Type -> Type -> Type

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


Сперва может показаться неплохой идеей объединить ~> и ->, так как оба означают тип (вид) функции. Проблема в том, что -> в позиции типа и -> в позиции вида означают разные вещи. На уровне термов, все функции из a в b имеют тип a -> b. На уровне типов же, только конструкторы из a в b имеют тип a -> b, но не синонимы типов и не семейства типов. В целях вывода типов, GHC предполагает, что из f a ~ g b следует f ~ g и a ~ b, что верно для конструкторов, но не для функций – оттого и ограничение.


Следовательно, чтобы повышать функции на уровень типов, но сохранить вывод типов, нам придется вынести конструкторы в отдельный тип. Назовем его a :-> b, для него действительно будет верно, что из f a ~ g b следует f ~ g и a ~ b. Остальные функции по-прежнему будут иметь тип a -> b. Например, Just :: a :-> Maybe a, но при этом isJust :: Maybe a -> Bool.


Когда с Demote будет покончено, последний шаг – избавиться от самого Sing. Для этого нам понадобится новый квантор, гибрид между forall и ->. Давайте посмотрим на функцию isJust повнимательнее:


isJust :: forall a. Maybe a -> Bool
isJust =
  \x ->
    case x of
      Nothing -> False
      Just _  -> True

Функция isJust параметризована типом a, а затем значением x :: Maybe a. Эти два параметра обладают различными свойствами:


  • Явность. В вызове isJust (Just "hello") мы передаем x = Just "hello" явно, а a = String выводится компилятором неявно. В современном Haskell мы также можем форсировать явную передачу обоих параметров: isJust @String (Just "hello").
  • Релевантность. Значение, передаваемое на вход в isJust в коде, будет передаваться и во время исполнения программы: мы выполняем сопоставление с образцом посредством case, чтобы проверить, это Nothing или Just. Потому значение считается релевантным. А вот его тип стирается и не подлежит сопоставлению с образцом: функция одинаково обрабатывает Maybe Int, Maybe String, Maybe Bool и т.д. Следовательно, он считается нерелевантным. Это свойство также называют параметричностью.
  • Зависимость. В forall a. t, тип t может упоминать a, и, следовательно, зависеть от конкретного переданного a. Например, isJust @String имеет тип Maybe String -> Bool, а isJust @Int имеет тип Maybe Int -> Bool. Это значит, что forall – зависимый квантор. Заметьте разницу с параметром-значением: не важно, вызовем ли мы isJust Nothing или isJust (Just …), тип результата всегда Bool. Следовательно, -> – это не зависимый квантор.

Чтобы выместить Sing, нам нужен квантор явный и релевантный, подобно a -> b, и в то же время зависимый, подобно forall (a :: k). t. Обозначим его как foreach (a :: k) -> t. Чтобы выместить SingI, также введем неявный релевантный зависимый квантор, foreach (a :: k). t. В результате singletons будут не нужны, так как мы только что добавили зависимые функции в язык.


Краткий взгляд на Haskell с зависимыми типами


С повышением функций на уровень типов и квантором foreach, мы сможем переписать lookupS следующим образом:


data N = Z | S N

len :: [a] -> N
len [] = Z
len (_:xs) = S (len xs)

data Fin n where
  FZ :: Fin (S n)
  FS :: Fin n -> Fin (S n)

lookupS :: foreach (xs :: [a]) -> Fin (len xs) -> a
lookupS [] = \case{}
lookupS (x:xs) =
  \case
    FZ -> x
    FS i' -> lookupS xs i'

Короче код не стал, все-таки singletons довольно неплохо прячет избыточный код. Однако новый код намного проще: больше нет Demote, SingKind, SList, SNil, SCons, fromSing. Нет использования TemplateHaskell, так как теперь мы можем вызывать функцию len напрямую вместо создания семейства типов Len. Производительность тоже будет лучше, так как больше не нужно преобразование fromSing.


Нам все еще приходится переопределять length как len, чтобы возвращать индуктивно определенный N вместо Int. Пожалуй, эту проблему лучше не рассматривать в рамках добавления зависимых типов в Haskell, ведь Agda тоже использует индуктивно определенный N в функции lookup.


В некоторых аспектах Haskell с зависимыми типами даже проще, чем стандартный Haskell. Все-таки в нем термы, типы и виды объединены в общий однородный язык. Я легко могу представить себе написание кода в таком стиле в коммерческом проекте, чтобы формально доказать правильность ключевых компонентов приложений. Многие библиотеки на Haskell смогут предоставить более безопасные интерфейсы без сложности, сопряженной с применением singletons.


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




Тезаурус


Термин
Перевод
Пояснение
correct by construction
Код, корректность которого гарантирована способом его составления
Методология разработки, согласно которой корректность кода гарантируется способом его составления (например, применением системы типов), а не тестированием.
memory unsafe
С небезопасным доступом к памяти
Возможность в языке программирования вручную выделять и освобождать память, выполнять арифметику с указателями.
unityped
Монотипизированный
Термин, который ввел Bob Harper для более точного описания языков, традиционно называемых динамически типизированными. В таких языках проверки меток типов отложены до времени выполнения программы.
boilerplate
Избыточный код
Однотипный код с похожими или повторяющимися элементами, который невозможно обобщить из-за недостаточной выразительности языка.
generics
Обобщенные типы
Возможность системы типов обобщить типы введением параметра. Например, вместо введения конкретных типов «СписокЧисел» и «СписокСтрок», можно ввести обобщенный тип Список, применяя его как Список<Число> и Список<Строка>.
runtime cast
Приведение типов времени выполнения
Преобразование значения одного типа в значение другого типа с проверкой во время выполнения программы.
effectful computation
Вычисление с побочными эффектами
Вычисление, выполнение которого приводит к наблюдаемым эффектам помимо возврата вычисленного значения.
composable
Композируемый
Характеристика кода, отмечающая простоту его применения в другом коде посредством операций композиции.
control structures
Конструкции, задающие поток управления
Конструкции языка, применение которых влияет на порядок вычисления подвыражений.
proof assistant
Средство доказательства теорем
Программное обеспечение для формального доказательства математических гипотез.
strict (eager) evaluation
Строгие (энергичные) вычисления
Стратегия вычисления выражений, согласно которой значения аргументов функции вычисляются до вызова функции.
backend
Бэкенд
Компонент компилятора, транслирующий внутреннее представление программы в код на целевом языке.
singleton type
Единичный тип
Тип, населенный одним значением, определяемым инстанцированием соответствующего параметра на уровне типов.
promoted definitions
Повышенные определения
Определения закрытых семейств типов, которые соответствуют тем или иным функциям на уровне термов.
Share post

Similar posts

AdBlock has stolen the banner, but banners are not teeth — they will be back

More
Ads

Comments 85

    +2

    Для всех кого заинтересовала данная тема, советую посмотреть на liquidhaskell.

      +1

      Там же refinement types, которые являются очень ограниченным подмножеством dependent types (что, впрочем, позволяет сделать их SMT-разрешимыми).

      –3

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

        +2
        А почему это будущее-то?

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

        У вас есть какие-то причины, почему они могут не быть полезны?)
          0

          Я эту мантру овердевятьтысяч раз из каждого холодильника уже слышал, и даже сам [в некотором приближении] с ней согласен. Просто, если «будущее» появляется в заголовке и тегах, можно как-то ну хотя бы попытаться что-нибудь похожее доказать (ну, типа).


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

            +4

            Ну вот вы в том числе больше ансейфа сможете сделать сейфом.

              0
              Больше статических гарантий — это очень хорошо, но в реальном мире у нас бизнес-логика все время лезет в ансейф, и все гарантии именно в трудных местах — идут лесом.

              Бизнес логика это весьма неоднозначное понятие, потому я не могу судить, о каких конкретно ограничениях вы говорите. Можете привести примеры?
                –2

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

                  0
                  Например, общение со сторонним провайдером данных, который эти самын данные генерирует левой пяткой.

                  Мы не можем гарантировать корректность внешней системы, внешнего мира.
                  В случае получения данных от внешней системы нам в любом случае придётся проверять их на уровне нашего приложения, а там уже некорректность обнаружится и обработается как предполагается.
                    +3

                    В этом случае вы можете гарантировать, что данные прошли валидацию.

                      –1

                      Прохождение валидации я и безо всяких типов могу гарантировать. Валидацию в любом случае надо будет написать, и это еще бабушка надвое сказала, что выгоднее: pattern-matching, или типы.

                        0
                        Валидацию в любом случае надо будет написать, и это еще бабушка надвое сказала, что выгоднее: pattern-matching, или типы

                        А они разве противоречат друг другу?

                          +3
                          Прохождение валидации я и безо всяких типов могу гарантировать.

                          Не так, потому что в обычных языках у вас прохождение валидации — это действие, а не значение.


                          и это еще бабушка надвое сказала, что выгоднее: pattern-matching, или типы.

                          А вы точно хотя б на хаскеле писали?

                            –3
                            Не так, потому что в обычных языках у вас прохождение валидации — это действие, а не значение.

                            Ох.


                            def preprocess(%{
                              foo: [:bar | _],
                              int: 42,
                              any: any,
                              nested: %{type: type} = nested
                            } = value) when type in [:a, :b], do: {:ok, value, {any, nested}}
                            def preprocess(value), do: {:error, value}

                            Действие, так действие.


                            А вы точно хотя б на хаскеле писали?

                            Да, но, как я говорил, это было в 2000–2003 и с тех пор я только научпоп почитываю. Я отдаю себе отчет в том, что могу не видеть за деревьями леса, но обычно (чисто статистически) внятные аргументы меня убеждают.


                            А противопоставление действий — значениям — нет.

                              +5
                              Действие, так действие.

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

                +2
                Хаскель это будущее или прошлое?

                Непонятно, но споры об этом идут уже почти 30 лет =)
                  +8

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

                    0
                    Очень поддерживаю. Я вот в хаскель наверное уже так никогда и не полезу (хотя конечно зарекаться не стоит), но когда плоды всей этой плавной эволюции докатятся в какой-нибудь typescript (а туда уже много что докатилось, на самом деле) — то я этим очень охотно буду пользоваться.
                      +2

                      Ну, я для себя решил все же попробовать. Приятно все-таки писать настолько безопасный и гибкий код, который на остальных языках начнут писать только через 5-10 лет. И людям все равно придется учить все те же концепции, когда они попадут во всякие Java/C++, но эти 5-10 лет они потеряют, пользуясь менее удобными инструментами.


                      В общем, каждому своё, мой выбор меня пока устраивает.

                        0
                        Нет, я с той стороны, что если есть желание именно разобраться с этим заранее, то брать именно хаскель — как-то, имхо, странно. Хаскель уже очень mature, он работает в проде, и из-за всего этого уже успел обрасти рядом компромиссов и разного «исторически так сложилось». Как тестовая площадка для обкатки крутых теоретических идей — это прекрасно, но именно с целью попрактиковаться в сильных типах я бы смотрел на то, что еще не обросло грузом исторического наследия.
                          +2

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


                          В хаскелле хватает "исторически сложилось", но если выбирать между ним и скалой, то в ML варианте получается сильно проще — по крайней мере после прочтения красной книги и курса по хаскелю на степике. Просто сравните:


                          val optionFunctor: Functor[Option] = new Functor[Option] {
                            def map[A,B](fa: Option[A])(f: A => Option[B]): Option[B] = fa match 
                              case None => None
                              case Some(x) => Some(f(x))
                          }

                          И


                          instance Functor Maybe where 
                             fmap _ Nothing = Nothing
                             fmap f (Just x) = Just (f x)

                          И это еще не говоря про сложности с имплиситами, отсутствием запрета на нечистые действия, и прочее, прочее...


                          В общем, возможно где-то есть более хорошие для изучения ФП языки, но я их не знаю.

                            +1

                            Ну, изучать всякую наркоманию на типах лучше таки в том же идрисе.

                              +1

                              А под него есть всякие идеи с автокомплитом и хуглом как для хаскеля? Потому как всё это важно.

                                0

                                Я пользуюсь idris-vim. Автокомплит уровня штатного вимовского (но лучше я не приделал и к хаскелю). Хугла нет (так как нет пакетного менеджера), но для изучения это и не нужно, имхо. Есть фичи типа case split, proof search, lift lemma, покажи-тип-дырки-и-контекст, которые в хаскеле у меня, считайте, вообще не заводились.


                                А у вас какое окружение для хаскеля? А то, может, я со своим vim + coc + hie отстал от жизни.

                                  +4

                                  Я пользуюсь идеей с плагином, причем на Windows. Умеет она всякое разное, например простенькие рефакторинги



                                  Подсказка типов (без необходимости писать дырку и спрашивать что за тип)



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


                                  Ну и в целом я не согласен с


                                  Хугла нет (так как нет пакетного менеджера), но для изучения это и не нужно, имхо.

                                  Как раз когда я начал пытаться склеить сервант с персистом я понял, зачем нужен МТЛ и трансформеры. До этого это было теоретическим знанием с игрушечными примерами "Обойдите дерево и сохраните сколько узлов вы обошли", а вот реальный пример позволяет прочувстввоать, что это и зачем.

                                    +1

                                    Лойс за Fira Code.


                                    А вообще прикольно, надо тоже попробовать. Я пробовал прикрутить плагин к CLion, оно установилось, но что-то не сработало. Попробую с голой Idea. vim, конечно, хорошо, но изолента проглядывает. И да, сколько это все счастье ест памяти? А то у меня hie счастливо десяток гигов на проект съесть может.


                                    например простенькие рефакторинги

                                    Это с hlint, или там свои диагностики?


                                    Подсказка типов (без необходимости писать дырку и спрашивать что за тип)

                                    Это полезно, да, в виме у меня такое не завелось.


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

                                    Это не только для новичка полезно, но и вообще, когда какую-то новую библиотеку используешь с хитрой структурой модулей.


                                    Как раз когда я начал пытаться склеить сервант с персистом я понял, зачем нужен МТЛ и трансформеры. До этого это было теоретическим знанием с игрушечными примерами "Обойдите дерево и сохраните сколько узлов вы обошли", а вот реальный пример позволяет прочувстввоать, что это и зачем.

                                    Это уже просто следующий уровень изучения.


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

                                      +1
                                      А вообще прикольно, надо тоже попробовать. Я пробовал прикрутить плагин к CLion, оно установилось, но что-то не сработало. Попробую с голой Idea. vim, конечно, хорошо, но изолента проглядывает. И да, сколько это все счастье ест памяти? А то у меня hie счастливо десяток гигов на проект съесть может.

                                      Ну я ничего крупного не открывал, но на моих маленьких крудах — 500мб.


                                      Это с hlint, или там свои диагностики?

                                      К сожалению понятия не имею. Оно жаст воркс, и глубже я не лезу. Из проблем только то что после изменение кабал/стак файла нужно перегружать репл. Но зависимости не так часто добавляются, так что жить можно.


                                      Это уже просто следующий уровень изучения.

                                      Но в него очень быстро упираешься. Сортировать числа и факториалы считать очень весело, но все же утомляет. А реальное приложение с БД без этих знаний не написать.


                                      Для хаскелля я нашел хороший курс на степике от Москвина. Для идриса таких не видел.

                                  0
                                  К редактору Atom есть плагин для Idris, мне нравится.
                                +1
                                Есть еще F# так-то)))
                          0
                          Учитывая, сколько фичей переехало из хаскеля в мейнстрим и продолжает перетекать, можно ответить философски: для кого прошлое, а для кого и будущее.

                          В общем-то из вещей специфичных именно для хаскеля очень мало что переехало. Если вообще хоть что-то, мне вот навскидку ничего в голову не приходит. Разве что тайпклассы в какой-то форме, ну и higher-kinds с их кодировками

                        +1
                        Ну кстати да… Заголовок «Зависимые типы в Haskell: почему это будущее разработки программного обеспечения» слишком уж общий. Типы-то в Haskell, а будущее в такой формулировке вроде как везде… Особенно с учетом того, что один из вариантов вовсе и не хаскель даже — не очень хорошая формулировка.
                          +1

                          Ну моё скромноо имхо в том, что это будущее всей разработки, но в разных языках это будущее наступит в разное время.

                            +2
                            Даже если мы все согласны, что это так — все равно про это тут не особо написано. Тут максимум два языка рассмотрены более-менее. А вывод про остальные откуда? Из этого поста, честно говоря, не следует даже что это будущее хаскеля — потому что три раза написано «проще сказать, чем сделать».
                        +1

                        Вряд ли вы добьетесь любви к Хаскелу у людей, которые его еще не любят (особенно пишущих на С и С++), используя фразы типа "Языки с небезопасным доступом к памяти, такие как C, приводят к самым серьезным ошибкам и уязвимостям (например, переполнение буфера, утечки памяти). Иногда такие языки нужны, но чаще всего их применение – идея так себе."


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

                          +3
                          Там ошибка только в том, что "но чаще всего" надо заменить на "но в других областях разработки".
                            +5
                            Ээ, а что не так-то? Это просто коснтатация факта — значительная часть уязвимостей и багов связаны с такого типа ошибками. И если 40 лет назад ещё можно было думать что это просто плохие программисты, то сегодня понятно что даже самые лучшие ошибаются.
                              +3
                              В смысле, они что, не приводят к ошибкам? Ну вообще мы такие ошибки все видели — так что это со стороны C/C++ скорее нужно доказывать, что на них как-то можно писать без ошибок, и поэтому хаскель не сильно нужен.
                                +2

                                Ну, я все же соглашусь, что надо писать повежливее. Когда вы начинаете разговор с "псс, парень, твой язык — хрень и кишит дырами" вы вряд ли сможете донести до него информацию о лучших инструментах, и будь вы 100 раз правы такая подача материала скорее всего загубит всю попытку.

                              +3

                              Не написано ничего (или я проглядел) про проблемы из-за ленивости и, в частности, из-за коданных. А они в хаскеле везде в идиоматичном коде.


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


                              Ну и называть агду эргономичной в мире, где есть идрис — ну такое.

                                +2
                                С другой стороны, хотя бы кодировка для них у нас есть!

                                Нет, ее нет. Зависимые типы, в отличии от каких-нибудь higher-kind, не кодируются в более слабых системах.
                                То, что описано далее — это простой лифтинг на уровень типов, возможный в любой системе с параметрическим полиморфизмом. Работает он только тогда, когда тип известен в компайлтайме.

                                  0

                                  А можно пример когда не работает? Вот у меня с консоли считывается булка и вполне себе на неё потом можно прицепить SBool: https://repl.it/@Pzixel/PowerfulBulkyLightweightprocess


                                  {-# LANGUAGE RankNTypes #-}
                                  {-# LANGUAGE KindSignatures #-}
                                  {-# LANGUAGE DataKinds #-}
                                  {-# LANGUAGE GADTs #-}
                                  
                                  data SBool (b :: Bool) where
                                    STrue :: SBool 'True
                                    SFalse :: SBool 'False
                                  
                                  fromSBool :: SBool b -> Bool
                                  fromSBool STrue  = True
                                  fromSBool SFalse = False
                                  
                                  data SomeSBool where
                                    SomeSBool :: SBool b -> SomeSBool
                                  
                                  withSomeBool :: SomeSBool -> (forall (b :: Bool) . SBool b -> r) -> r
                                  withSomeBool (SomeSBool sbool) f = f sbool
                                  
                                  toSomeBool :: Bool -> SomeSBool
                                  toSomeBool True   = SomeSBool STrue
                                  toSomeBool False  = SomeSBool SFalse
                                  
                                  main = do
                                    b <- readLn
                                    let 
                                      someBool = toSomeBool b
                                      bool = withSomeBool someBool fromSBool
                                    putStrLn (show bool)
                                    +2

                                    Ну GADTs — это очень базовая симуляция некоторых фишек, не более. Да, вы таскаете с собой свидетеля, и паттерн-матчингом по нему можете что-то восстановить. Но обратите внимание, что SBool — другой тип, не Bool, что язык термов на уровне типов вы использовать не можете, и так далее.


                                    Как пример того, что ломается на практике — да хоть вот https://stackoverflow.com/questions/52750918/lifting-existentials-to-type-level

                                      0

                                      Все работает, если постараться :) https://gist.github.com/int-index/743ad7b9fcc54c9602b4eecdbdca34b5

                                        0

                                        Ужас какой. Ну вот, теперь мне надо вспоминать, где я там полтора года назад во что конкретно упёрся.


                                        Но спасибо за ваш вариант, типы в хаскеле — это как шаблоны в C++, существуют варианты лучше, но есть что-то мазохистично-приятное в них.

                                      +1

                                      Максимум, что позволяет подобная кодировка — это "расщепить" типы по паттерн-матчингу. Ну т.е. как если бы у тебя в АТД каждый элемент суммы был как бы отдельным типом (как это, допустим, в тайпскрипте происходит, когда ты пишешь что-то вроде type Yoba = { type: 'Foo' } | { type: 'Bar' }), то type Foo = { type: 'Foo' } и type Bar = { type: 'Bar' } — это сами отдельные типы. С-но, ты можешь сделать кейз на тип и потом где-то дальше уже знать, что твое значение это не какой-то непонятный Yoba, а вполне себе конкретный Foo (т.е. значение соответствует паттерну, и этот факт выражается в типе — ты можешь сформулировать тип которому принадлежат только те значения, что соответствуют паттерну). Но на этом все.

                                        +1

                                        Ну мне тут в контрпримером бросились, такое ощущение, что можно: https://gist.github.com/Nexmean/56c98ff9563ff25a05b70512a7de6848

                                          +1
                                          Не понял, этот контрпример что должен доказать конкретно? Где там зав. типы?
                                          Для зав. типов надо уметь параметризовать тип термом. В данном случае мы можем параметризовать тип термом, который можно вычислить в компайл тайме (лифтанув этот терм в типы). Но мы не можем параметризовать тип термом, который в компайлтайме неизвестен.

                                          Т.е. ты можешь написать vector<5> или vector<10>.
                                          Ты можешь написать vector<*>, где * неизвестно (при этом эффективно vector<*> будет означать тип всех векторов), считать этот вектор, а потом разматчить этот вектор на vector<5>, vector<10>, vector<Greater<5>> и т.п.
                                          Но ты не можешь написать vector<*>, где * у тебя переменная в локальном скопе.
                                          Обрати внимание на определяющую разницу с предыдущим пунктом — в первом случае vector<*> это _любой_ вектор, а во втором — это конкретный вектор с конкретным *, которого мы не знаем (но который будет однозначно фиксирован в момент исполнения).
                                            0

                                            Как это не можем? Вот мы число с консольки считываем, как по мне это вполне считается за границу "неизвестное значение".

                                              +2
                                              > Как это не можем?

                                              Ну напиши :)
                                              Ты вот в примере выше с булями если считаешь подряд два булевых значения, то у них будут одинаковые типы. А если ты считаешь два булевых значения с dependent types — типы будут разные. И ты сможешь написать ф-ю test, которая, например, будет чекаться если були равны и не будет — если они не равны.

                                              > Вот мы число с консольки считываем, как по мне это вполне считается за границу «неизвестное значение».

                                              Ну вот тут оно будет «какое-то число», а в зависимых типах — «конкретное число». В случае «конкретное число» ты сможешь, например, сделать vectorRef с k < n, а в случае «какое-то число» операция vectorRef будет запрещена для любого k. Т.е. ты можешь создать vector, но при этом ничего с таким вектором не сможешь сделать. Тебе сначала надо будет преобразовать его к какому-нибудь более конкретному типу.
                                                0

                                                А как сделать Fin n, где n это узнаем в рантайм. У bool только два типа, поэтому сделать матч значение в тип можно, а для бесконечных множеств как? Нужен чтобы каждый вызов функции создавал новый тип, как ефекты в идрисе.

                                                  0

                                                  Я после bool еще один пример скинул, там вполне себе Fin n

                                                    0

                                                    Так это то же самое что bool только с рекурсией. Всё равно у вас функция которая аргументу сопоставляет тип. А мне кажется надо выдавать именно что уникальный тип. Иначе я не понимаю как это работает, вот вы считываете А и В, они получается в рантайме конкретный тип получают по своему значению? А какой тогда тип у А + В, как доказать что А + B больше А для натуральных чисел?

                                      –1
                                      Вообще, от Idris у меня впечатление «на этом уже можно программировать». От Хаскела такого нет. Но сейчас радует язык Factor, он весёлый и смешной, давайте все на него перейдём.
                                        +1
                                        Вообще, от Idris у меня впечатление «на этом уже можно программировать». От Хаскела такого нет.

                                        Интересное впечатление. Там же библиотек нет, пакетного менеджера нет (ну или есть четыре зачаточных, как смотреть), производительность Idris 1 куда хуже ghc. Ну и сахара в хаскеле сильно больше.

                                          0

                                          Хм. А были какие-то движения в сторону поддержки haskell кода? Я к тому что ФП языков мало, и если бы я захотел написать новый, я бы взял в рассчёт некоторую совместимость с более популярными языками.

                                            +4

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


                                            1. Поддерживать современный хаскель как он реализован в ghc, со всеми используемыми расширениями системы типов — очень нетривиальная задача, так как построить адекватную метатеорию всей этой ерунды с доказательством полезных для верифицированного программирования свойств, скажем так, очень нетривиально.
                                            2. Поддерживать чистый Haskell2010 без всех расширений? А на нём никто уже не пишет. Вернее, даже если вы пишете на этом языке, то, скорее всего, на нём не пишут авторы используемых вами библиотек.
                                            3. Даже если вы вдруг решите поддерживать чистый Haskell2010, то это будет тоже очень нетривиально, потому что все эти зависимо типизированные языки с возможностью доказательств очень сильно опираются на некоторые вещи, которые в хаскеле сделаны, ну, совсем по-другому (например, хаскель не различает данные и коданные, и это больно, в хаскеле есть undefined, в хаскеле нет требований strict positivity на типы данных, и прочая, прочая, прочая).

                                            Или, если вкратце, совместимым с хаскелем быть можно, но это резко меняет направленность языка. И хаскель, в который добавят завтипы, не будет «полноценным идрисом».

                                              0
                                              например, хаскель не различает данные и коданные

                                              Почему не различает? Есть же strictness аннотации. Все, что с ними — это данные, без них — коданные.


                                              И хаскель, в который добавят завтипы, не будет «полноценным идрисом».

                                              Refinement типы можно добавить. Будет все, что можно сделать на зависимых, но только проще и удобнее.

                                                0

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


                                                Почти все имеющиеся библиотеки основаны на обычном [], который не пойми что. Это в каком-то смысле общий интерфейсный для всех тип, который очень больно будет менять.

                                                  0
                                                  который не пойми что

                                                  Почему не пойми что? Вы можете на, допустим, агде без коиндукции написать аналог хаскелевского []? Нет. Значит, это коиндуктивный тип. Как и все вообще типы хаскеля без strictness аннотаций. data Nat = Zero | Succ x — тоже коиндуктивный, например. Тут, конечно, тот момент что x seq f(x) это не совсем то же самое, что и force, но по факту это детали реализации.

                                                    +1

                                                    Ну когда у вас все типы эффективно коиндуктивные, то что-то в языке не так.

                                                  0

                                                  Увидел правку только сейчас.


                                                  Refinement типы можно добавить. Будет все, что можно сделать на зависимых, но только проще и удобнее.

                                                  Ну ведь далеко не все же. RT — очень ограниченное подмножество.

                                          0
                                          Я за этим всем слежу с начала 80-х, когда писал диплом на функциональном языке GARF, который сочинил боговдохновенный Илья Ханаанович Шмаин (потом он уехал в Израиль, а потом вернулся и стал православным священником). Краткое описание языка GARF, подаренное В.Б.Борщёвым (не уверен, можно ли что-то понять)
                                          mega.nz/#!PrInzYAa!zPnzW6Dj4hRQz5qJSPFBnnC5YCAII_1-9eFZuj2qYs8
                                          и краткая биография Шмаина
                                          mega.nz/#!XjBHmKBB!qh7Bme8Zx1_rOPWFNOERtm-59_tVTxjTPg6zpyVrkbU
                                          Ссылки копировать целиком (почему-то плохо вставляются)
                                            +1
                                            И вот тогда это вызывало энтузиазм, а теперь что-то всё меньше и меньше. В идеале программы надо представлять как-то графически, типа узла из цветных ниток, который вязать виртуальным крючком. Но если бы я знал, как.
                                              +1
                                              Попыток сделать графический язык программирования было немало. Всякий раз реализация упирается в то, что сколько-нибудь серьёзные программы не умещаются на экране и потому совершенно теряют в наглядности (не говоря уже о отсутствии нормального тулинга).
                                                +1
                                                Есть более серьёзные попытки. Самые быстрые на сегодня способы вычислять лямбда-термы — это вычислительные схемы (рисуются радиодетальки, соединённые проводками, схема по определённым правилам перестраивается, подробности можно почитать в книге Asperti, Guerrini
                                                gen.lib.rus.ec/book/index.php?md5=43A67A9BF71F483E34879816454E04EF
                                                но чтение не простое). Но эти схемы не наглядны с самого начала, даже маленькие. С другой стороны, у категорщиков теперь есть пруфчекер Globular, позволяющий строить доказательства о категориях в виде картинок в графическом редакторе
                                                golem.ph.utexas.edu/category/2015/12/globular.html
                                                (на картинки полюбуйтесь, даже узел из ниток получается).
                                                  0

                                                  А в текстовом виде будто умещаются.
                                                  И тулинг – дело наживное.

                                              +1
                                              … джазмен выкладывается на полную, одну, пьесу, вторую, третью… Один из братков подходит к сцене и сочувственно так:
                                              — Что, братишка, не получается?
                                                –3
                                                Ничто в этих сигнатурах типов не отражает требования, что индекс должен быть неотрицательным и меньше длины коллекции

                                                А в Pascal диапазоны есть издревле:


                                                С Педивикии
                                                const
                                                  minlist = 1;
                                                  maxlist = 5;
                                                  maxword = 7;
                                                
                                                type
                                                  listrange = minlist .. maxlist;
                                                  wordrange = 1..maxword;
                                                  word = record
                                                    contents: packed array [wordrange] of char;
                                                    length: wordrange
                                                  end;
                                                  wordlist = array[listrange] of word;
                                                var
                                                  i: integer;
                                                  words: wordlist;
                                                
                                                procedure CreateList(var w: wordlist);
                                                begin
                                                  w[1].contents := 'print  ';
                                                  w[1].length := 5;
                                                  w[2].contents := 'out    ';
                                                  w[2].length := 3;
                                                  w[3].contents := 'the    ';
                                                  w[3].length := 3;
                                                  w[4].contents := 'text   ';
                                                  w[4].length := 4;
                                                  w[5].contents := 'message';
                                                  w[5].length := 7;
                                                end;
                                                
                                                begin
                                                  CreateList(words);
                                                  for i := minlist to maxlist do
                                                    with words[i] do
                                                      WriteLn(contents: length);
                                                  for i := maxlist downto minlist do
                                                    with words[i] do
                                                      WriteLn(contents: length)
                                                end.

                                                В который раз убеждаюсь, что паскалиное семейство незаслуженно забыто. Относительно C язык довольно безопасный: указатели строго типизированные, массивы защищены от выхода за границы. При этом не генерирует огромные бинари, как Go и Haskell, и не компилируется полчаса, поливая матом код до полного прилизывания, как Rust. А Lazarus вдобавок позволяет делать графические приложения, которые прозрачно собираются с GTK+ или Qt, удовлетворяя тулкитофобов обоих лагерей. Что ещё нужно для счастья?

                                                  0
                                                  А в Pascal диапазоны есть издревле:

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

                                                    0

                                                    Да там даже со значениями в компайл тайм не всё гладко.

                                                    0

                                                    Ну не знаю, я вот спокойно записал по индексу 0 и 55 два значения, и меня компилятор не остановил.


                                                    https://rextester.com/CMIB62735

                                                      0

                                                      Главное, что сегфолта нету. И компилятор таки ругается.


                                                      @bq:00:42:39:/tmp/dl$ fpc a.pas
                                                      Free Pascal Compiler version 3.0.4+dfsg-23 [2019/11/25] for x86_64
                                                      Copyright (c) 1993-2017 by Florian Klaempfl and others
                                                      Target OS: Linux for x86-64
                                                      Compiling a.pas
                                                      a.pas(20,5) Warning: range check error while evaluating constants (0 must be between 1 and 5)
                                                      a.pas(32,5) Warning: range check error while evaluating constants (55 must be between 1 and 5)
                                                      Linking a
                                                      /usr/bin/ld.bfd: предупреждение: link.res содержит выходные разделы; забыли указать -T?
                                                      43 lines compiled, 0.5 sec
                                                      2 warning(s) issued
                                                        0

                                                        И есть ключик для более строгой проверки.


                                                        @bq:00:46:44:/tmp/dl$ fpc -Cr a.pas
                                                        Free Pascal Compiler version 3.0.4+dfsg-23 [2019/11/25] for x86_64
                                                        Copyright (c) 1993-2017 by Florian Klaempfl and others
                                                        Target OS: Linux for x86-64
                                                        Compiling a.pas
                                                        a.pas(20,5) Error: range check error while evaluating constants (0 must be between 1 and 5)
                                                        a.pas(32,5) Error: range check error while evaluating constants (55 must be between 1 and 5)
                                                        a.pas(44) Fatal: There were 2 errors compiling module, stopping
                                                        Fatal: Compilation aborted
                                                        Error: /usr/bin/ppcx64 returned an error exitcode
                                                          0

                                                          Ну, это кстати неплохо.


                                                          А можно вместо константы использовать аргумент? Например, чтобы CreateList была не процедурой, а функцией, и возвращала массив длины n для передавнного зачения n. Тогда он тоже скажет что значение вышло за границы?


                                                          Главное, что сегфолта нету.

                                                          В этом только не уверен. Запись мимо массива — это очень нехорошо. Если компилятор конечно не вырезал этот код нафиг, но он вроде так не должен делать.

                                                            0

                                                            С массивами динамической длины в Pascal отдельная песня. Зато есть директива { $R }, прозрачно включающая проверки диапазонов по всему коду.

                                                      0
                                                      К сожалению моё образование не позволяет ничего понять, но если я правильно понял дискуссии выше, то там идёт обсуждение о том как на стадии компиляции гарантировать, что индекс не выйдёт за пределы массива, при том что значение индекса будет известно только в рантайме — мне кажется это в принципе невозможно.
                                                      Или есть какая-то математическая магия которая хотя бы частично это покрывает?
                                                        +1
                                                        как на стадии компиляции гарантировать, что индекс не выйдёт за пределы массива, при том что значение индекса будет известно только в рантайме — мне кажется это в принципе невозможно.

                                                        Можно гарантировать, что сделана проверка на выход за пределы.

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

                                                            Нет, наличие проверки статически гарантируется.

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

                                                                Реальный индекс может быть известен только в рантайме. Но гарантируя наличие проверки мы гарантируем что выхода за границы при обращении не будет.
                                                                  +1

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

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

                                                                    А есть какой-то способ без проверок рантайма доказать, что произвольное считанное число не выходит за границы? :)
                                                                    Где-то проверка будет, просто не обязательно прямо в месте обращения к элементу массива.

                                                                      0

                                                                      А кто сказал, что оно именно произвольное? В простейшем случае, например, вы просто пробегаете по всем элементам от 0 до длины массива.

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

                                                        Only users with full accounts can post comments. Log in, please.