LINUX.ORG.RU

Основывая на чём можно выбрать OCamL или Erlang или Haskell


0

5

Я догадываюсь, что это какая-то паранойа !!! Но как !?

Конечно очевидный вариант - попробовать все. И подумать.

Пробую... Думаю... А дальше что ???

OCamL похож на F#, красив и удобен... хорошо. Применять можно везде, к web имеет много забавных наработок.

Erlang имеет достаточно мощную, стабильную виртуальную машину и синтаксис очень забавный ! Интересный web server yaws и NoSQL DBMS.

Haskell выигрывает по полярности и там есть много действительно хороших библиотек вообще в любой сфере...

Отвечаю на первый предугаданный вопрос - нет, я не хочу на них писать драйвера. Мне интересны сайты, промышленные приложения, утилиты... Но в любом случае я не понимаю как можно их сравнить и выбрать один. Если есть люди, которые выбрали - расскажите как ?


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

Например:

Shriram Krishnamurthi. Programming Languages: Application and Interpretation

A type is any property of a program that we can establish without executing the program. In particular, types capture the intuition above that we would like to predict a program’s behavior without executing it.

Это конечно половина правды. Вот ещё:

Franklyn Turbak, David Gifford, Mark A. Sheldon. Design Concepts in Programming Languages

Types naturally arise from the fact that certain values can be meaningfully used only in certain contexts. For this reason, almost all programming languages support some notion of type and a type system for reasoning about types. The chief purpose of a type system is to detect type errors — attempts to perform an inappropriate operation on a value. Examples of type errors are adding an integer and a string, calling a procedure with the incorrect number and/or types of arguments, calling an integer as a procedure, and interpreting the bits of a floating point number as an integer, a memory address, or a machine instruction. Some type systems detect type errors when the program is executed, while others detect them when the program is analyzed before it is executed (see Section 11.3.1). We say that a programming language is type-safe if its type system prevents attempts to perform inappropriate operations. It might do this by aborting program execution when a type error is detected at run time, or by aborting program compilation when a type error is detected at compile time.

...

Languages in which all values conceptually carry type annotations that can be inspected at run time are said to be dynamically typed or latently typed.The process of inspecting type information at run time is called dynamic type checking. ... In implementations of dynamically typed languages, dynamic type checking incurs both space and time costs at run time: Space is necessary to encode the type of a value at the bit level, and inspecting these types when performing certain primitive operations takes time.

...

An alternative to processing types at run time is to statically analyze a pro- gram before executing it to determine whether type information is consistent. The process of analyzing the types of phrases is called static type checking, and languages using this approach are said to be statically typed. In static type checking, types are associated with phrases in the language rather than with run- time values. If types can be consistently assigned to all of its phrases, a program is said to be well typed. Typically, well-typed programs are guaranteed not to encounter type errors at run time, because all such errors should have been discovered during static type checking.

Т.е. можно иметь типы и в рантайме, но как «run-time values» - просто значения того же языка, а не как «phrases in the language» - не в виде языка типов отдельного от языка значений.

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

quasimoto ★★★★
()

Бородатый тролль, прикидывающийся бабой + вброс на тему маргинальных языков = PROFIT + 9 страниц срача.

// капча setVisible кагбэ намекаеэт на вывод на чистую воду.

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

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

Нет, типы чекаются во время компиляции.

Во всех трёх случаях _нужно_ что-то генерировать

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

в третьем слуае у нас есть type level с конструкторами типов. Вот я и спрашиваю - что делать в динамическом языке без type level-а?

А зачем надо что-то делать? В динамической ЯП все функции изначально полиморфны, неполиморфных ф-й нет.

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

> Формальныя семантика никак не запрещает использовать:

Скажем так, ф-и, которая бы выдирала значение изнутри ИО, просто в конетксте хаскеля никакой семантики придать нельзя.

Вы пишете что, если бы сделали стрелочный интерфейс к IO, то все бы юзали стрелки

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

при том, что стрелочный интерфейс к IO это нонсенс.

Ну и что?

Я к тому что костыли это костыли, они не нуждаются в обоснованиях. Обосновывают обычно концепции, идеологии и удобные модели.

Наоборот.

Таких статей как для SystemFC - нет.

То есть их система типов никаких спек не имеет? Лесом тогда.

Систему для core language берут заведомо мощнее - не только чтобы реализовать haskell98, но и какие-то расширения.

Так я и спрашиваю - зачем? core language может быть вообще нетипизирован, это нам не помешает реализовать что угодно с любыми расширениями поверх него. А так получается - система типов мощная, но никакого эффекта это не дает т.к. мы этой системы не видим. Странно, в общем.

То что у JHC core language больше чем у GHC значит, что, в принципе, там можно реализовать больше расширений системы типов.

Нет, не значит.

А, ну да. Если типы алгебраичны для этого нужно чтобы (if :: Bool -> a -> b -> a :| b) и писать нужно (if pred (L 1) (R «1»))

Если объединения есть, то можно просто писать (if pred 1 «1»), тип будет Number U String.

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

Нет, типы чекаются во время компиляции.

Это хорошо. Т.е. базовый язык должен быть динамическим без каких-то выделенных типов (только значения, в т.ч. ФВП) и работать на гетерогенном стековом рантайме где всё что движется тегировано. А компилятор этого языка должен предоставлять средства вроде макросов для реализации статических DSL с compile time системами типов, работающих поверх динамического языка. Как если бы мы взяли лисповый VM (лисповую машину) и на ней делали как динамические так и статические языки. Это довольно интересно (в racket-е, например), но тут тоже есть свои недостатки - эти DSL-и будут несовместимы друг с другом; писать/выбирать типизированные DSL-и это не то чем должен заниматься программист (должна быть _одна_, но хорошая система типов); у нас машины не гетерогенные стековые, а гомогенные регистровые, поэтому лучше брать такую VM; реализация статического языка поверх динамического на гетерогенной стековой VM будет менее эффективеной чем реализация со специально выбраным гомогенным регистровым VM; с другой стороны динамические языки можно делать на основе статических (CL в CMUCL/SBCL - средний уровень с выведенными типами статически типизирован, рантайм регистровый, работающий с тегированными объектами).

Темплейты с++, темплейты с++, темплейты с++... сколько мне еще раз это повторить, чтобы ты понял?

Блин, заняться самообразованием я всегда могу. Я конкретно тебя спрашиваю как это сделать в racket-e/CL (шаблоны в C++ ведь на рантайм повязаны - это не просто надстройка).

динамической ЯП все функции изначально полиморфны, неполиморфных ф-й нет.

_Параметрически_ полиморфны? Нет ведь. (Int -> Int) матчится со схемой (t -> t), а (Char -> Int) - нет, это параметрический полиморфизм. В случае динамического полиморфизма - матчатся оба варианта.

Так я и спрашиваю - зачем? core language может быть вообще нетипизирован, это нам не помешает реализовать что угодно с любыми расширениями поверх него. А так получается - система типов мощная, но никакого эффекта это не дает т.к. мы этой системы не видим. Странно, в общем.

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

Нет, не значит.

Почему? Вот GHC перешёл на более мощный внутренний язык - это позволило реализовать новые расширения.

Если объединения есть, то можно просто писать (if pred 1 «1»), тип будет Number U String.

Только при сабтайпинге вида (x < x + y) и (y < x + y) ((<) - отношение для подтипов, (+) - конструктор для типов сумм (объединений то есть)). Без сабтайпинга придётся делать отображения (x -> x + y) и (y -> x + y). Только такой сабтайпинг порушит всю безопасность типов (по крайней мере в хаскеле).

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

> но тут тоже есть свои недостатки - эти DSL-и будут несовместимы друг с другом;

Ну typed racket как раз и делается так, чтобы быть полностью совместимым с нетипизированным диалектом (ну вплоть до того, что прямо в модуль на обычном racket можно вставить кусок типизированного кода). Собственно, по этой причине он и делается медленно, если бы не вопрос совместимости - написать чекер для system f omega задача на неделю максимум.

писать/выбирать типизированные DSL-и это не то чем должен заниматься программист (должна быть _одна_, но хорошая система типов);

Как раз нет. Суть в том и есть, что система типов не должна быть прибита к языку, программист должен иметь возможность выбрать ту систему типов, возможности которой ему нужны на данный момент. Не существует никакой хорошей системы типов, «хорошесть» в данном случае понятие относительное. Для одного случая хороша одна система, для другого - другая. Не нужны для текущего модуля гарантии корректности - пишем без типов, нужны - добавляем типы, причем мощность системы должна гибко варьироваться от того, каких гарантий мы хотим. Ну а со стороны языка должен предоставляться своего рода фреймворк, который позволит все эти модули объединить.

у нас машины не гетерогенные стековые, а гомогенные регистровые, поэтому лучше брать такую VM;

Ну вообще да, желательно, оптимальный вариант для вм на мой взгляд - это поддержка system f с подтипированием на уровне рантайма (ну типа как в шарпе, например, больше никаких подобных вм пока не существует, насколько я знаю).

Блин, заняться самообразованием я всегда могу. Я конкретно тебя спрашиваю как это сделать в racket-e/CL (шаблоны в C++ ведь на рантайм повязаны - это не просто надстройка).

Блин, в том же хаскеле type erasure, то есть полиморфные ф-и на уровне рантайма не поддерживаются. Другими словами, после компиляции полиморфных ф-й нет, то есть оно реально работает практически так же как плюсовые шаблоны. Мы не можем скомпилировать полиморфную ф-ю/структуру, но можем скомпилировать ее конкретный инстанс, а в программе у нас и участвуют всегда конкретные инстансы. Плюсовый темплейт - это просто частный случай макроса, в конкретном месте в этот темплейт подставляется типовой аргумент и мы получаем обычный неполиморфный код. В cl/racket-е это делать _не надо_. Как я уже говорил, параметрический полиморфизм поддерживается в динамических языках по умолчанию (там все ф-и полиморфны по всем своим аргументам). Вот если у нас статически типизированный ЯП без полиморфизма, то тогда полиморфизм через макросы легко вводится (собственно, как его в плюсах и ввели).

_Параметрически_ полиморфны? Нет ведь. (Int -> Int) матчится со схемой (t -> t), а (Char -> Int) - нет

Ну он матчится со схемой t1 -> t2.

Вот как раз в первом абзаце писал. Лучше брать конкретную систему типов и конкретную VM под неё, чем супер универсальную гетерогенную VM над которой _возможно_

Ну для эффективной реализации, вообще говоря, достаточно обычной лямбда-стрелки. ВМ, которые хоть где-то используют более мощные возможности системы типов пока что и нет (кроме упомянутого .net/mono). Зачем может понадобиться поддержка тех же зависимых типов со стороны рантайма - я даже в теории представить не могу.

Почему? Вот GHC перешёл на более мощный внутренний язык - это позволило реализовать новые расширения.

Ну их и так можно было реализовать. Видимо тут проблема конкретно в архитектуре GHC.

Только при сабтайпинге вида

Ну это единственно верный сабтайпинг и есть.

Только такой сабтайпинг порушит всю безопасность типов (по крайней мере в хаскеле).

Ну в хаскеле вообще сабтайпинга нет (для ограниченной квантификации сделали кривой костыль - тайпклассы). И не будет никогда, я полагаю.

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

Ну typed racket как раз и делается так, чтобы быть полностью совместимым с нетипизированным диалектом

А у typed racket есть спеки на систему типов?

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

Вроде с этим немного понятнее стало. В динамическом языке аргументы имеют универсальный тип T (субтипом которого является любой другой тип) и возвращаемое значение - тоже типа T. То есть передавать в функцию можно что угодно - динамический полиморфизм. А если мы хотим зафиксировать у функции параметрически полиморфную схему (a -> a) - можно это сделать контрактами (assert-ами), либо нарисовать систему типов на макросах. Короче, всё свелось к тому что на динамически типизированном языке с хорошими макросами можно реализовать произвольный DSL. Непосредственно с помощью динамического полиморфизма нельзя (!) использовать параметрически полиморфные схемы (рантайм assert-ы я не учитываю).

Только при сабтайпинге вида

Ну это единственно верный сабтайпинг и есть.

Я там не совсем правильно выразился - сабтайпинг будет нужен только для обычной (if :: Bool -> t -> t -> t), если отображение в сумму типов делать внутри if:

if' :: Bool -> a -> b -> a `Either` b
if' True  x _ = Left x
if' False _ y = Right y

то можно так и писать (if' True 1 «2»), а чтобы унифицированно использовать значения возвращаемые этим if нужно построить бифункторный интерфейс (вот, кстати, пример когда монадический интерфейс никак не подходит):

import Control.Arrow

(<|) :: (a -> a') -> Either a b -> Either a' b
(<|) f = f +++ id

(|>) :: Either a b -> (b -> b') -> Either a b'
(|>) = flip $ (+++) id

-- (+ 1) <| (if' True 1 "2") |> (++ "!") ,
-- > 2
-- 
-- (+ 1) <| (if' False 1 "2") |> (++ "!")
-- > "2!"

Ну в хаскеле вообще сабтайпинга нет (для ограниченной квантификации сделали кривой костыль - тайпклассы). И не будет никогда, я полагаю.

В HList occurrence subtyping сделан как раз с помощью type level программирования на классах (мультипараметричных с функциональными зависимостями и гибкими инстансами). GHC-шные классы типов это считай правила логического вывода (логические высказывания - выражения на type level языке), тут и до SystemF<: недалеко.

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

> А у typed racket есть спеки на систему типов?

Там обычная полиморфная лямбда с парой расширений, специфичный для лиспо-функцийй (например, лисповый «+» нельзя вообще ни в какой системе лямбда-куба типизировать).

сабтайпинг будет нужен только для обычной

Ну это ясно.

В HList occurrence subtyping сделан как

Там нету сабтайпинга. В хаскеле вообще нельзя выразить ничего вроде «a есть подтип b». Можно в некотором смысле сабтайпинг эмулировать, используя другие средства, но сабтайпингом это не будет.

GHC-шные классы типов это считай правила логического вывода (логические высказывания - выражения на type level языке), тут и до SystemF<: недалеко.

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

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

Ну для полноценного ЯП чекер написать несколько сложнее (чисто механически), чем для обычного лямбда-исчисления.

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

Там обычная полиморфная лямбда с парой расширений, специфичный для лиспо-функцийй (например, лисповый «+» нельзя вообще ни в какой системе лямбда-куба типизировать).

Ну а в JHC обычная PTS :) (а про PTS нужно читать, видимо, у Barendregt).

Про typed racket нашёл спеку - в «The Design and Implementation of Typed Scheme».

Там нету сабтайпинга. В хаскеле вообще нельзя выразить ничего вроде «a есть подтип b». Можно в некотором смысле сабтайпинг эмулировать, используя другие средства, но сабтайпингом это не будет.

А можете привести какую-нибудь модельную задачу? Чтобы были конкретные ADT, и сабтайпинг сыграл какую-то роль. Чтобы можно было видеть, что, да, вот тут на хаскеле никак нельзя написать такой код как в динамическом языке с сабтайпингом.

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

Ну для полноценного ЯП чекер написать несколько сложнее (чисто механически), чем для обычного лямбда-исчисления.

А в чём будет отличие? Добавятся литералы и некоторые специальные формы - let, letrec, case, cast, может ещё что-то, так что придётся добавить соответствующие ветви в typeCheck. Ну и ещё код может распухнуть из-за того что Expr будет содержать аннотации, а переменные разную вспомогательную информацию (про модули, id для эффективности, про места объявления и т.п.).

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

Например, задачка про LSP и эллипс + круг.

-- -----------------------------------------------------------------------------
-- * Subtyping relation on types.
-- -----------------------------------------------------------------------------

infixr 0 $>, $>$

-- | `a' is subtype of `b'.
class a :< b where
  -- | Pass function through subtyping scheme (e.g. aggregation or inheritance 
  -- scheme).
  ($>)  :: (b -> c) -> a -> c
  ($>$) :: (b -> b) -> a -> a
  -- | Declare subtyping relation.
  subType :: a -> b -> ()
  subType _ _ = ()

(:<) - это отношения для подтипов. subType может декларировать такое отношение. ($>) и ($>$) определяются в инстансах и устанавливают как функции распространяются по схеме подтипов (например - агрегации или наследования). И вот эллипс + круг с использованием схемы агрегации:

-- -----------------------------------------------------------------------------
-- * Circle-ellipse problem.
-- -----------------------------------------------------------------------------

type R = Float

-- |
-- Aggregation scheme:
-- 
--   R ---> Point <----- R
--            |
--           (:>)
--            v
--          Circle <---- R
--            |
--           (:>)
--            |
--            v
--          Ellipse <--- R
-- 

-- | Point := R * R
data Point = Point { x :: R, y :: R }
  deriving ( Eq, Read, Show )

-- | Circle := Point * R
data Circle = Circle { center :: Point, radius :: R }
  deriving ( Eq, Read, Show )

-- | Ellipse := Circle * R
data Ellipse = Ellipse { circle :: Circle, radius' :: R }
  deriving ( Eq, Read, Show )

-- | Circle is subtype of point.
instance (:<) Circle Point where
  f $> c = f $ center c
  f $>$ (Circle p r) = Circle (f p) r

-- | Ellipse is subtype of point.
instance (:<) Ellipse Point where
  f $> e = f $> circle e
  f $>$ (Ellipse c r) = Ellipse (f $>$ c) r

-- | Ellipse is subtype of circle.
instance (:<) Ellipse Circle where
  f $> e = f $ circle e
  f $>$ (Ellipse c r) = Ellipse (f c) r

move :: Point -> Point -> Point
move (Point dx dy) (Point x y) = Point (x + dx) (y + dy)

-- | Test LSP:
-- 
--   ∀ (x : T). q(x) => ∀ (y : S <: T). q(y)
-- 
test = let
  circle = Circle (Point 1.0 1.0) 2.0
  ellipse = Ellipse circle 3.0
  in do
    -- LSP about center:
    print $ center circle
    print $ center $> ellipse
    -- LSP about radius:
    print $ radius circle
    print $ radius $> ellipse
    -- Just plain function:
    print $ radius' ellipse
    -- LSP about move:
    print $ move (Point 1.0 2.0) $>$ circle
    print $ move (Point 1.0 2.0) $>$ ellipse

-- test
-- >
-- Point {x = 1.0, y = 1.0}
-- Point {x = 1.0, y = 1.0}
-- 2.0
-- 2.0
-- 3.0
-- Circle {center = Point {x = 2.0, y = 3.0}, radius = 2.0}
-- Ellipse {circle = Circle {center = Point {x = 2.0, y = 3.0}, radius = 2.0}, radius' = 3.0}

(почему «Ellipse is subtype of circle»: если наоборот, то это нарушит LSP - например, эллипс можно вертеть, а окружность нельзя. Тоже самое с «Circle/Ellipse is subtype of point» - круг и эллипс можно растягивать, а точку - нет).

Т.е., как говорят, ADT is OOP done right, но когда речь заходит о сабтайпинге и LSP, то всё сводится к построению схемы агрегации для ADT и настраиванию инстансов (:<) вместе с комбинаторами распространения функций по схеме агрегации.

А если нужно делать отношение на типах, то можно определить такой тип:

data a :< b

Тогда (Int :< Integer) будет отдельным типом. Потом определяем класс вычисляющий такие типы в compile time:

class SubTypeRelation ab r | ab -> r

ну и дальше инстансы какие-то:

instance SubTypeRelation (a :< (a `Either` b)) a
instance SubTypeRelation (b :< (a `Either` b)) b

__ = __

test = __ :: SubTypeRelation (Int :< (Int `Either` Char)) r => r

-- :t test
-- > test :: Int
quasimoto ★★★★
()
Ответ на: комментарий от quasimoto

> Ну а в JHC обычная PTS :)

Ну так в том и дело, что такого понятия как «обычная PTS» не существует. В том смысле, что любая из существующих систем типов - это обычная PTS :)

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

Если есть сабтайпинг, то язык уже не динамический :)

А можете привести какую-нибудь модельную задачу? Чтобы были конкретные ADT, и сабтайпинг сыграл какую-то роль.

Ну вот есть у нас два класса, один - наследует другому. В хаскеле это выразить невозможно :)

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

> А в чём будет отличие?

Я же говорю - чисто механически. Но на практике как раз эта сложность и преодолевается 90% времени, затраченного на написание чего-либо.

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

> (:<) - это отношения для подтипов. subType может декларировать такое отношение. ($>) и ($>$) определяются в инстансах и устанавливают как функции распространяются по схеме подтипов (например - агрегации или наследования). И вот эллипс + круг с использованием схемы агрегации:

Никто и не спорил, что на хаскеле можно написать интерпретатор ЯП с подтипированием. У вас отношение подтипирования разрешается в рантайме, если вы не заметили (функции >$ $>$). Вот если бы эти ф-и срабатывали в компайлтайме - это бы было походе (только похоже) на сабтайпинг, а так - ничего общего. И еще - как при такой реализации будет выглядеть ограниченная квантификация? То есть если у меня есть полиморфная ф-я forall a. a -> a и я хочу наложить ограничение, чтобы a было только подтипом некоторого x (ну по аналогии с тем, как можно потребовать от a реализации некоего тайпкласса)?

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

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

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

Ну вот есть у нас два класса, один - наследует другому. В хаскеле это выразить невозможно :)

То есть? class A t => B t - и есть такое выражение. Или про какие классы речь?

У вас отношение подтипирования разрешается в рантайме, если вы не заметили (функции >$ $>$).

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

И еще - как при такой реализации будет выглядеть ограниченная квантификация? То есть если у меня есть полиморфная ф-я forall a. a -> a и я хочу наложить ограничение, чтобы a было только подтипом некоторого x (ну по аналогии с тем, как можно потребовать от a реализации некоего тайпкласса)?

foo :: (a :< x) => a -> a

А ну и самое важное - отношение подтипов на, собственно, типах никому особенно и не нужно

Ну я сталкивался на практике с тем, что может быть удобно для сложной схемы агрегации написать инстансов для (:<) и унифицировано вызывать методы, а не тянутся каждый раз по разным аккессорам.

покажите сабтайпинг для интерфейсов (то есть для тайпклассов). То есть как, например, выразить тот факт, что Integral есть подкласс Num?

А вот с такой необходимостью - не сталкивался :) Ну кроме непосредственной записи class (Num a, Ord a) => Real a; class (Real a, Enum a) => Integral a. Вообще typeclasses - далеко не first class values. Даже обычные типы - не совсем first class values. Причём если типы становятся first class values, то классы типов становятся как таковые не нужны.

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

У вас отношение подтипирования разрешается в рантайме, если вы не заметили (функции >$ $>$)

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

-- | Subtyping relation on types: (a :< b) means `a' is subtype of `b'.
class a :< b where
  -- | Return superobject for object of type `a'.
  sup :: a -> b
  {-# INLINE sup #-}
  -- | Return subobject for object of type `b'.
  sub :: b -> a
  {-# INLINE sub #-}
  sub = undefined
  -- | Apply combinator, return value of free type `c'.
  ($>) :: (b -> c) -> a -> c
  {-# INLINE ($>) #-}
  f $> x = f $ sup x
  -- | Apply combinator, return value of type `a'.
  ($>$) :: (b -> b) -> a -> a
  {-# INLINE ($>$) #-}
  f $>$ x = sub $ f $ sup x
  -- | Declare subtyping relation.
  subType :: a -> b -> ()
  subType _ _ = ()

instance (:<) a a where
  sup = id
  sub = id

{- WTF?
instance (a :< b, b :< c) => (:<) a c where
  sup x = sup (sup x :: b)
  sub x = sub (sub x :: b)
 -}
quasimoto ★★★★
()
Ответ на: комментарий от quasimoto

> То есть? class A t => B t - и есть такое выражение.

Нет.

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

Я, может, немного не так выразился. Суть в том, что само подтипирование определяется в рантайме, а вот конкретный тип выбирается в компайл-тайме. В то время как все должно быть наоборот. Ну вот если у вас есть ф-я f: Point -> Point, теперь делаем map f [circle, ellipse] - оно ведь не будет работать, так? И нет способа заставить заработать.

foo :: (a :< x) => a -> a

А транзитивность отношения учитывается?

А вот с такой необходимостью - не сталкивался :)

Угу, потому что в рамках системы тайпклассов это вообще никакого смысла не имеет :)

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

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

А должны быть одинаковые :) Именно по-этому это не сабтайпинг.

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

То есть? class A t => B t - и есть такое выражение.

Нет.

Это мистика. На каком основании тогда можно высказаться о том что один CLOS класс наследуется от другого? На основе символьной информации и макросов? В хаскеле есть Language.Haskell.TH.Syntax.Name вместо символов и reify :: Name -> Q Info, где

data Info
  = ClassI Dec
  | ClassOpI Name Type Name Fixity
  | ...

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

data Dec
  = ...
  | ClassD Cxt Name [TyVarBndr] [FunDep] [Dec]
  | InstanceD Cxt Type [Dec]
  | ...

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

Почему наоборот? «Конкретный тип выбирается в рантайме» - это наводит на мысли о языковой рефлексии (type-of который умеет работать сам по себе исходя из чего-то вроде RTTI), т.е. как в динамических языках (лиспы) или в статических снабжённых top type-ом (Java, F#). Хаскель - он не такой. Так что ситуация с выбором типа во время компиляции тут наоборот нормальная (иначе почти нельзя, разве что у нас есть параметрически полиморфный тип, и в скопе Typeable - тогда можно делать typeOf, но это имеет ограниченное применение).

Ну вот если у вас есть ф-я f: Point -> Point, теперь делаем map f [circle, ellipse] - оно ведь не будет работать, так?

Как раз прямо так и будет работать. Ну то есть hMap f $ circle :# ellipse :# empty - нужно использовать гетерогенные функции.

А транзитивность отношения учитывается?

Схема настраивается вручную, так что нет. Чтобы учитывалось нужно больше type levela добавить - просто (instance (a :< b, b :< c) => (:<) a c ...) работать не будет.

А должны быть одинаковые :) Именно по-этому это не сабтайпинг.

Ненужно. Мне нужны разные :) f $> object, при этом object :: a, а f :: b -> c, т.е. f может действовать на какой-то подобъект на произвольном уровне вложенности - естественно будет подставлена нужная (в зависимости от конкретного типа) последовательность аккесоров (чтобы дотянутся до того подъобкте. Весь этот пример это в первую очередь структурный сабтайпинг - т.е. схема типов совпадает (инверсно) со схемой агрегирования. Хотя ничего не мешает использовать такой интерфейс как-то иначе.

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

> На каком основании тогда можно высказаться о том что один CLOS класс наследуется от другого?

Ни на каком, динамика же.

Можно узнать всю информацию о наследовании

Нельзя по одно простой причине - наследования в хаскеле нет. А невозможно узнать информацию о том, чего нет.

Почему наоборот? «Конкретный тип выбирается в рантайме»

Потому что таково формальное определение сабтайпинга. При выборе в компайлтайме мы вместо сабтайпинга получаем параметрический полиморфизм. Тут проблема в том, что формально это вещи ортогональные, но юз-кейзы у них сильно пересекаются (ну вплоть до того, что сабтайпинг в ООП называют полиморфизмом).

Так что ситуация с выбором типа во время компиляции тут наоборот нормальная

Да я и не говорил, что она ненормальная. Просто это не сабтайпинг, а параметрический полиморфизм, вот и все. Сабтайпинга в хаскеле нет и быть не может. Потому что «хаскель - он не такой» :)

Ну то есть hMap f $ circle :# ellipse :# empty - нужно использовать гетерогенные функции.

Я и говорю - не раотает. А вот с сабтайпингом - работает.

Ненужно. Мне нужны разные :)

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

естественно будет подставлена нужная (в зависимости от конкретного типа) последовательность аккесоров

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

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

Ни на каком, динамика же.

Неправильно - на основании MOP :) Но это тоже динамика.

Нельзя по одно простой причине - наследования в хаскеле нет. А невозможно узнать информацию о том, чего нет.

Ну вы приводили пример с классами Num и Integral, так что я подумал, что под «наследованием» понимаются контексты. Наследования в смысле SystemF<: - да, нет.

«Конкретный тип выбирается в рантайме»

Потому что таково формальное определение сабтайпинга.

Это где такое определение? В википедийной статье вообще про это ничего. Или вот формальная SystemF<: - там ведь отношение наследования тоже времени компиляции (времени проверки схем наследования и типов).

При выборе в компайлтайме мы вместо сабтайпинга получаем параметрический полиморфизм.

Просто это не сабтайпинг, а параметрический полиморфизм, вот и все.

Классы хаскеля разве имеют какое-то отношение к параметрческому полиморфизму? Это ad-hoc полиморфизм - то что позволяет делать ограниченную квантификацию и, как следствие, record subtyping.

Я и говорю - не раотает. А вот с сабтайпингом - работает.

Тут дело вовсе не в сабтайпинге, а в том что вы написали [circle, ellipse] - опять нонсенс, т.е. объекты разного типа в гомогенном списке. Хотите иметь списки из объектов разного типа - берите гетерогенные HList.

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

Типа (+ (read) (read))? Или о чём речь? Если всё типобезопасное вынесено за IO, то все типы можно вывести.

Хотя это и не совсем удобно. Например, если f :: A a => a -> b и g :: A a => b -> a, то (f . g :: b -> b) хоть и имеет конкретный смысл - определить её нельзя, если не ввести диспетчеризацию в рантайме (выбор конкретного метода).

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

Т.е. SystemF:> = параметрический полиморфизм + ограниченная квантификация, SystemFC = параметрический полиморфизм + классы типов (ad hoc полиморфизм).

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

Например, если f :: A a => a -> b и g :: A a => b -> a, то (f . g :: b -> b) хоть и имеет конкретный смысл - определить её нельзя, если не ввести диспетчеризацию в рантайме (выбор конкретного метода).

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

Пусть есть два любых типа a и b (они будут объектами моделируемой категории):

∀ (a :: *), (b :: *).                                       -- рассуждения справедливы для любых двух типов

Тут forall-квантификация, то есть нужен параметрический полиморфизм. (::) - отношение типизации (можно сказать - устройство ассоциированной PTS), (*) - kind для универсума типов.

Термы этих типов задаются просто как множества (непредикативно):

  {t_i(a) :: a}_i = 1 .. |a|                                -- все термы типа `a'
  {t_i(b) :: b}_i = 1 .. |b|                                -- все термы типа `b'

|a| означает мощность типа a, т.е. количество термов этого типа (оно может быть конечным, счётным, либо несчётным). Все конструктивные способы задания термов данного типа это любые модели индуктивных типов - ADTs, GADTs, indexed families и т.п.

Дальше проводим квантфикацию по всем классам (т.е. супертипам, или семействам типов у которых kind уже (**)):

  ∀ (с :: **).                                              -- рассуждения справедливы для любых классов
    {p_i :: c}_i = 1 .. |c|                                 -- все типы данного семейства, |c| - количество типов в семействе
    {t_k(p_i) :: p_i}_k = 1 .. |p_i|, i = 1 .. |c|          -- все термы этих типов

Пусть 0 - терминальный объект, 1 - начальный объект, ⊥ := 0 : 1 -> 0 - bottom value, а (+) - ко-произведение (сумма типов, объединение).

Замечание: (:) - обозначение стрелки (отличается от отношения типизации), (:=) - определение терма (в алгоритмическом смысле).

Возьмём два семейства функций:

    {f_i : a -> p_i + 0}_i = 1 .. n, n ≤ |c|                -- семейство стрелок из `a' в подмножество семейства типов `c'
    {g_i : p_i + 0 -> b + 0}_i = 1 .. m, m ≤ |c|            -- семейство стрелок из подмножества (другого) семейства типов `c' в тип `b'

  картинка:

      i = 1 .. n, n ≤ |c|
      k = 1 .. m, m ≤ |c|

      a       p_i           p_k       b
      . ---->  .  --|id|-->  .  ----> .

Теперь введём обобщённые функции f (как обощение первого семейства) и g (второго).

f будет такой:

    f : a -> ⅀ p_i + 0

            ,  f_1(x), ¬ f_1(x) :: 0
            |  f_2(x), ¬ f_2(x) :: 0
    f(x) := <  ...
            |  f_n(x), ¬ f_n(x) :: 0
            `  0, otherwise

на уровне реализации это может быть также:

            ,  f_1(x), f_1(x) ≠ 0
            |  f_2(x), f_2(x) ≠ 0
    f(x) := <  ...
            |  f_n(x), f_n(x) ≠ 0
            `  0, otherwise

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

Теперь, какой тут появляется смысл - динамические «достаточно широкие» типы моделируются с помощью ко-произведений, то есть типов сум (⅀ p_i + 0). Смысл f - применять частичные функции f_i на своём аргументе до получения полезного значения. Функции вида f часто встречаются в динамических языках - например лисповый read, который может возвращать объекты разных типов (но не обязательно разные значения для разных аргументов - "(1 . ())" и "(1)" разбираются одинаково), пример в хаскеле - парсеры составленные с помощью комбинатора (<|>) работают по такой же схеме. В каких-то конкретных случаях f может быть реализована иначе (и более эффективно, чем просто пробовать разные функции-спецификации на своём аргументе до получения полезного значения), но иметь такой же математческий смысл как определение f выше.

Обобщение семейства g_i будет таким:

    g : ⅀ p_i + 0 -> b

            ,  g_1(x), x :: p_1
            |  g_2(x), x :: p_2
    g(x) := <  ...
            |  g_m(x), x :: p_m
            `  0, otherwise

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

typeOf : ∀ (t : *), (a : t). a -> t

Смысл g - динамическая рантайм диспетчеризация методов. В зависимости от типа аргумента (typecase в динамическом языке) выбирается конкретная специфичная функция g_i.

Наконец, определим динамические аналоги комбинаторов композиции (.) и аппликации ($).

Статические выглядят так:

(.) : (b -> c) × (a -> b) -> (a -> c)             -- я не использую каррирования, чтобы не связываться с экспоненциалами в CCC :)
(.) f g := Lam x (App f (App g x))                -- (.) выражается через примитивы LC

id : ∀ (a : *). a -> a
id x := x

($) : (a -> b) -> (a -> b)                        -- ($) выражается через (.)
($) f := f . id

При этом композиция

g . f : a -> b

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

{cod(f_i : a -> p_i + 0)}_i = 1 .. n, n ≤ |c|    =    {dom(g_i : p_i + 0 -> b + 0)}_i = 1 .. m, m ≤ |c|

но мы точно знаем, что в данном случае ничего плохого не случится и при соблюдении более слабого условия:

{cod(f_i : a -> p_i + 0)}_i = 1 .. n, n ≤ |c|    ⊆    {dom(g_i : p_i + 0 -> b + 0)}_i = 1 .. m, m ≤ |c|

и тут в дело вступает сабтайпинг, мы вводим два правила для подтипов:

x <: x + 0

⅀_K p_i <: ⅀_L p_i  iff  K ⊆ L

и «динамические» комбинаторы композиции и аппликации:

(.<:) : (b <: b'). (b' -> c) × (a -> b) -> (a -> c)

($<:) : (a -> b) -> (a -> b)
($<:) f := f .<: id                                         -- ($<:) тоже выражается через (.<:)!

Небольшой пример - нет ничего плохого в комбинации двух функций (f : t -> a + b) и (g : a + b + c -> t'), при этом (g . f) не определена, но определена, причём типобезопасно, (g .<: f). Нужно иметь ввиду, что (.<:) должна уметь расставлять конструкторы тех типов для которых определены правила подтипирования, например, для этого примера, g .<: f := g . L . f. В общем случае можно утверждать, что динамический комбинатор композиции (.<:) выражается через свой элементарный аналог (.) (который, в свою очередь, выражается через примитвы лямбда исчисления) и конструкторы типов учавствующих в отношениях подтипирования. Весь функциональный код с использованем комбинаторов (.<:) и ($<:) можно назвать динамически типизированным, а обычный, с комбинаторами (.) и ($), - статически типизированным.

Вообщем, такой оксюморон - динамическая типобезопасная система типов :)

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

> Это где такое определение?

Ну можно взять тапл, например. При сабтайпинге мы во время компиляции знаем, что X - некоторый подтип Y, но не знаем _какой именно подтип_. По-этому в рантайме подтип на этом месте может оказаться любой. В хаскеле так нельзя, в хаскеле всегда подтип известен при компиляции, по-этому программа, корректная при сабтайпинге может быть некорректна при эмуляции в хаскеле (например список, элементы которого могут иметь любой тип, являющийся подтипом данного и эти типы могут быть перемешаны, в хаскеле мы сможем выразить только список одного конкретного подтипа, если только не использовать экзистенциальные типы, которые вообще вещь ортогональная).

Классы хаскеля разве имеют какое-то отношение к параметрческому полиморфизму? Это ad-hoc полиморфизм - то что позволяет делать ограниченную квантификацию и, как следствие, record subtyping.

Вообще да - не обязательно параметрический полиморфизм, сразу и параметрический и ad-hoc. Нам важно что для полиморфной ф-и выбирается конкретный инстанс, а какова структура этого инстанса (одинакова для всех типов как при параметрическом полиморфизме или разная при ad-hoc) нам не важно.

Тут дело вовсе не в сабтайпинге, а в том что вы написали [circle, ellipse] - опять нонсенс,

Так вот как раз дело в сабтайпинге. С точки зрения сабтайпинга такой список будет иметь тип List circle, список гомогенный, никаких проблем. Это и есть отличие сабтайпинга от полиморфизма, именно в этом суть сабтайпинга, именно этот факт делает системы с сабтайпингом более выразительными, чем системы без сабтайпинга.

Хотите иметь списки из объектов разного типа - берите гетерогенные HList.

С точки зрения компилятора при сабтайпнге этот список самый что ни на есть гомогенный.

Типа (+ (read) (read))? Или о чём речь? Если всё типобезопасное вынесено за IO, то все типы можно вывести.

Нельзя. Если у нас есть ф-я f: x -> y (x,y - монотипы), то при сабтайпинге в рантайме на месте x и y может оказаться любой подтип/супертип ч/у соответственно и _какой именно_ нету никакого способа узнать.

если не ввести диспетчеризацию в рантайме (выбор конкретного метода).

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

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

> Т.е. SystemF:> = параметрический полиморфизм + ограниченная квантификация,

+ сабтайпинг

SystemFC = параметрический полиморфизм + классы типов (ad hoc полиморфизм).

+ ограниченная квантификация (вырожденный случай)

anonymous
()

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

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

у меня глаза от CL болят )

Да и на Haskell-то много проектов делают и развивается он быстро, вот с OCamL действительно как-то непонятно.

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

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

У меня болели пока не понял зачем нужно pretty printing и как его читать.

Рекомендую вот на это обратить свой взор http://habrahabr.ru/blogs/development/127635/ Это почему я считаю языки вроде haskell и ocaml не очень хорошими.

Hexs
()

Единственный шанс лисперов перестать стать полезной и более-менее популярной технологией - побросать свои SBCL-и и CMUCL-и и целыми днями пилить ECL. Но нет же, вместо этого лиспоиды предпочитают задрачивать псевдоакадемические опердени, а проблемы потребления памяти, поломанных API и интегрируемости с целевой ОС их абсолютно не волнуют.

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