LINUX.ORG.RU

[haskell][news] GHC 7.4

 ,


1

2

Уже была новость про RC. -XSafe, -XTrustworthy, -XUnsafe, -XPolyKinds, compiler plugins.

Ещё из новых возможностей - в GHCi теперь кроме функций можно давать любые определения (data, type, newtype, class, instance, deriving, foreign). Функции по-прежнему требуют подставлять let (как в do-блоке, может, в будущем уберут такое поведение).

-XConstraintKinds (заметка в блоге автора). Если -XPolyKinds не очень много меняет - просто позволяет писать чуть более строго типизированный type-level код, то -XConstraintKinds - несколько более мощное расширение. Оно добавляет новый kind - Constraint. Если все типы объединяются в kind *, то все классы типов объединяются в kind Constraint, более того, теперь можно проводить forall квантификацию не только по типам (:: *), но и по классам типов (:: Constraint). Например, теперь можно делать динамическую диспетчеризацию (позднее связывание) и Dynamic-like типы более удобно.

Пример.

module Shape where

-- * Объекты (типы данных).

data Circle = Circle Double
  deriving ( Show, Eq )

data Square = Square Double
  deriving ( Show, Eq )

-- * Интерфейс (набор методов).

class ShapeInterface a where
  perimeter :: a -> Double
  area :: a -> Double

-- * Реализация интерфейса (определения методов).

instance ShapeInterface Circle where
  perimeter (Circle r) = 2 * pi * r
  area (Circle r) = pi * r * r

instance ShapeInterface Square where
  perimeter (Square s) = 4 * s
  area (Square s) = s * s

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

{-# LANGUAGE ExistentialQuantification #-}

module ShapeDynamic where

import Shape

-- * Динамический тип -- обвёртка с помощью existential quantification.

data Shape = forall a. ShapeInterface a => Shape a

-- * Реализация интерфейса для динамического типа.

instance ShapeInterface Shape where
  perimeter (Shape x) = perimeter x
  area (Shape x) = area x

-- * Умные конструкторы для динамических объектов.

circle :: Double -> Shape
circle = Shape . Circle

square :: Double -> Shape
square = Shape . Square

-- * Использование.

shapes :: [Shape]
shapes = [circle 2, square 3]

example :: [Double]
example = map area shapes

-- shapes
-- > No instance for (Show Shape)

-- example
-- > [12.566370614359172,9.0]

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

Если после вдруг окажется, что кроме ShapeInterface нужны другие интерфейсы, то нужно возвращаться и править обвёртку. Либо писать обвёртку на каждый интерфейс (а это адъ). Например, чтобы добавить интерфейс Show:

data Shape = forall a. (Show a, ShapeInterface a) => Shape a

instance Show Shape where
  show (Shape x) = show x

-- shapes
-- > [Circle 2.0,Square 3.0]

Теперь, с помощью -XConstraintKinds, можно написать так:

{-# LANGUAGE Rank2Types, KindSignatures, GADTs, ConstraintKinds,
             FlexibleInstances, UndecidableInstances #-}

module ShapeDynamicNew where

import GHC.Prim ( Constraint )

import Shape

-- * Общее место.

-- | Dynamic строит тип (*) из одно-параметрического класса типов
-- (* -> Constraint). Класс типов передаётся как аргумент конструктору типов.
-- Конструктор данных принимает любые объекты разделяющие интерфейс данного
-- класса типов и возвращает динамический объект построенного типа Dynamic cls.
data Dynamic :: (* -> Constraint) -> * where
  Dynamic :: forall cls a. cls a => a -> Dynamic cls

-- * Складываем необходимые интерфейсы.

class (Show t, ShapeInterface t) => ShowShapeInterface t
instance (Show t, ShapeInterface t) => ShowShapeInterface t

-- * Динамический тип -- все те объекты которые разделяют данный интерфейс(ы).

type Shape = Dynamic ShowShapeInterface

-- * Реализация интерфейса для динамического типа.

instance ShapeInterface Shape where
  perimeter (Dynamic x) = perimeter x
  area (Dynamic x) = area x

instance Show Shape where
  show (Dynamic x) = show x

-- Умные конструкторы для динамических объектов.

circle :: Double -> Shape
circle = Dynamic . Circle

square :: Double -> Shape
square = Dynamic . Square

-- * Использование.

shapes :: [Shape]
shapes = [circle 2.0, square 3.0]

example :: [Double]
example = map area shapes

-- shapes
-- > [Circle 2.0,Square 3.0]

-- example
-- > [12.566370614359172,9.0]
★★★★

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

А в википедии написано, что constraints типам.

Какие constraints и каким типам?

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

Вот именно. Не минимальному, а любому.

Жопа это не класс.

Ну да, это тип.

И да, жопы в виде типа в хаскеле нет.

По факту-то есть. Значение _|_ принадлежит любому типу, следовательно, тип _|_ является подтипом любого типа. Так?

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

Clojure слишком функциональная по сравнению со Scala? Да ты шутишь.

Здорово ты перевернул мои слова. Я имел ввиду, что кроме ФП мне нужно еще развитое ООП. В Scala есть и то, и другое. Clojure много не смотрел. Может там, с ООП тоже полный порядок, но у меня есть некоторые сомнения на сей счет.

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

Я тут пропустил, в каком смысле «минимальный»?

Минимальный подтип.

Например

(type-of 0) => BIT
(typep 0 'fixnum) => T
(subtypep 'bit 'fixnum) => T T

bit <: fixnum, т.е. bit - подтип fixnum и минимальный тип для 0 среди всех типов 0 связанных отношением подтипирования. Максимальный тип, т.е. супертип для всех типов, у всех один - t.

С другой стороны

(type-of 5) => (INTEGER 0 536870911)
(typep 5 '(integer 0 5)) => T
(subtypep '(integer 0 5) '(integer 0 536870911)) => T T

тут не минимальный.

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

Какие constraints и каким типам?

Constraints образуемые классами типов, типам ad-hoc полиморфных функций.

Параметрически полиморфная сигнатура:

forall (t :: *). t -> t -> Bool

и ad-hoc полиморфная:

Eq (t :: *) => t -> t -> Bool

т.е. forall это квантификация по универсуму малых типов (*, Set, U₀), а Eq это квантификация по ad-hoc составленному множеству типов-инстансов класса Eq (подмножество универсума малых типов). Дальше вопрос терминологии - называть отношение принадлежности типов множеству типов образуемому инстансами класса отношением типизации, или нет. Я такую терминологию («да, называть») не принимаю. Я просто боюсь за консистентность модели, некое «кое-как» (т.е. ad-hoc) составленное подмножество универсума считать под-универсумом и вводить для него отношение типизации - не знаю. Пусть это будет отношение инстанцирования :)

На нормальную модель можно посмотреть в agde:

data Eq : Set → Set ...

_==_ : (t : Set) → (eqT : Eq t) → t → t → Bool
...

дальше, для удобства, остаются только (технические) implicit и instance arguments:

_==_ : {t : Set} → ⦃eqT : Eq t⦄ → t → t → Bool
...

лишних сущностей нет - классов типов, квантификаций и т.п., есть inductive families, иерархия универсумов и зависимые типы.

Ну да, это тип.

А нам нужен класс - т.е. если у тебя типы принадлежат классам (как типам типов), то на множестве этих классов (на решётке) должен быть минимальный и максимальный класс, а их нет.

Значение _|_ принадлежит любому типу, следовательно, тип _|_ является подтипом любого типа. Так?

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

True :: forall a. (a ~ Bool) => a
undefined :: forall a. a

в котором достижим undefined и возможны не тотальные функции вроде

f :: forall a. Bool -> a
f True = f True

Категорно:

true : 1 → bool
false : 1 → bool
undefined : (a : Obj) → 0

технически (без представления начальных и терминальных объектов в языке) и получается:

true : bool
false : bool
undefined : (a : Type)

как в хаскеле. В (2-)категории f будет выглядеть так:

f : bool → (a : Obj)
eval(f) : f ∘ true ⇒ f ∘ true

редукция (2-стрелка) такова, что f это не терминируемая функция.

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

Здорово ты перевернул мои слова.

Неправильно тебя понял.

Clojure много не смотрел. Может там, с ООП тоже полный порядок, но у меня есть некоторые сомнения на сей счет.

http://www.coderanch.com/t/482531/clojure/Incubator/Does-Clojure-support-OOP

Ну и это все-таки лисп, с макросами =)

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

Меня смущает вот это:

But i think that [OOP] would go against the principles of language.

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

Я такую терминологию («да, называть») не принимаю.

Ну ты можешь принимать или не принимать что угодно, однако по факту мы получаем систему типов.

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

А его не надо вводить. Оно введено уже тем самым, что мы это подмножество выделили. Если у нас есть некоторое покрытие множества - то у нас есть система типов. Ведь система типов это и есть ни что иное как некоторое покрытие множества. Вводя те или иные ограничения этого покрытия, получаем системы типов с теми или иными свойствами.

А нам нужен класс - т.е. если у тебя типы принадлежат классам (как типам типов), то на множестве этих классов (на решётке) должен быть минимальный и максимальный класс, а их нет.

Максимальный класс - Any, он есть (forall a. a - сокращение для forall a. (Any a) => a), минимальный класс - пересечение всех классов, для любой программы он тоже строится. Не вижу проблем.

Индуктивному типу принадлежат только те значения, которые выводимы из его индуктивного определения.

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

Например, тип Bool имеет в качестве термов только True и False - больше ничего

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

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

Максимальный класс - Any

Not in scope: type constructor or class `Any'

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

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

значит любой терм потенциально виснет

Напиши пример программы в которой Bool «зависнет». Только не перепутай Bool с полиморфными типами.

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

Not in scope: type constructor or class `Any'

Кстати, Typeable можно бы было счесть за такой Any, но есть 100500 типов, у которых нет инстансов Typeable.

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

Напиши пример программы в которой Bool «зависнет». Только не перепутай Bool с полиморфными типами.

all even (map (2*) [1..])

Not in scope: type constructor or class `Any'

Это ты к чему?

Если только так - дописать программу до того, чтобы можно было утверждать, что «да, отношение инстанцирования тут = вариант отношения типизации», а до тех пор, в любой взятой программе

Зачем дописывать, не понял? По факту в любой программе в любой момент написания тайпкласс-пересечение все определенных в программе тайпклассов есть. Так в чем проблема?

а до тех пор, в любой взятой программе, это будет просто отношение инстанцирования.

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

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

Кстати, Typeable можно бы было счесть за такой Any, но есть 100500 типов, у которых нет инстансов Typeable.

Однако, нет ни одного типа, который бы не был инстансом Any. Например, имеем id :: forall a. (Any a) => a -> a, из определения сразу следует, что тип тогда и только тогда не будет инстансом Any, когда id неприменима к этому типу. Назови такой тип.

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

all even (map (2*) [1..])

Тут не Bool, а codata зависли. Достаточно было сказать, что [0 ..] не возвращает управление. А индуктивные типы _данных_ никак не связаны с undefined (просто из любого типа есть единственный терм в терминальный тип - терм undefined).

Это ты к чему?

Ну вот ты рассуждаешь:

Однако, нет ни одного типа, который бы не был инстансом Any. Например, имеем id :: forall a. (Any a) => a -> a, из определения сразу следует, что тип тогда и только тогда не будет инстансом Any, когда id неприменима к этому типу. Назови такой тип.

But WTF is @Any@?

Так в чем проблема?

В том, что sup и inf таки отсутствуют, в общем случае.

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

Тут не Bool, а codata зависли.

Да никого не интересует, что именно зависло. Есть некий терм, он имеет определенный тип. Если он имеет тип Bool, то этот терм обязан вернуть Bool, он не может зависнуть. А если терм зависает - значит его тип жопа. Следовательно, если терм может вернуть Bool, а может и зависнуть - его тип Bool U жопа. Это просто факты.

But WTF is @Any@?

Any - весь универсум типов, очевидно.

В том, что sup и inf таки отсутствуют, в общем случае.

Как это? Только что мы убедились, что в любом случае они есть. Как они могут отсутствовать? Приведи пример, где они отсутствуют.

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

его тип Bool U жопа.

Ну и опять - WTF is @жопа@? Что это за имя в Prelude / Whatever? Нет такого типа -> это умозрительное рассуждение.

Приведи пример, где они отсутствуют.

Любая программа на хаскеле :) Я говорю, Any / whatever нету в base -> их нужно дописывать -> их нет. В общем случае ты не сможешь дописать иерархию классов до того чтобы всегда были sup и inf классы (причём, конкретные, как имена из какого-то модуля, а не умозрительные).

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

По факту-то есть. Значение _|_ принадлежит любому типу, следовательно, тип _|_ является подтипом любого типа. Так?

Пусть так. undefined :: Bool. По факту - undefined : Bool + _|_.

Осталось выяснить - всегда ли существуют inf и sup классы. Как конкретные классы (не вижу таких)? Или, опять по факту, их можно умозрительно достроить/дописать - тогда пусть так.

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

Ну и опять - WTF is @жопа@?

Это тип, который соответствует зависающему терму.

Что это за имя в Prelude / Whatever?

В Prelude / Whatever нет никакого такого имени.

Нет такого типа -> это умозрительное рассуждение.

Как нету? Хочешь сказать, что у терма all even (map (2+) [1..]) нету терма? Это же чушь.

Любая программа на хаскеле :) Я говорю, Any / whatever нету в base -> их нужно дописывать -> их нет.

Бред какой-то. При чем тут дописаны они или нет? Тип есть, если он есть, а не если кто-то там что-то там дописал. «Дописывание» - условие достаточное, но никак не необходимое.

В общем случае ты не сможешь дописать иерархию классов до того чтобы всегда были sup и inf классы (причём, конкретные, как имена из какого-то модуля, а не умозрительные).

Как это не могу? Для любой программы эти типы есть и дописать их можно. Значит - могу. Конечно, никто не гарантирует, что эти тпы для разных программ будут совпадать - но нам этого и не надо. Нам нужны Top/Bottom для каждой конкретной программы.

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

Осталось выяснить - всегда ли существуют inf и sup классы. Как конкретные классы (не вижу таких)?

Вопрос в том, что понимать под существованием. Если есть некий тайпкласс, то мы можем объявить тайпкласс пересечение, так? Значит, тайпклассы-пересечения существует - вне зависимости от того, являются ли они _уже_ объявленными. Если тип объявлен - это значит, что тип существует и с ним ассоциировано некоторое имя. Но тип может существовать и без имени, очевидно же. Вот мы пишем forall a. (X a, Y a) => a, тип (X a, Y a) есть? Есть. Объявлен? Нет.

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

Хочешь сказать, что у терма all even (map (2+) [1..]) нету терма?

Нету типа.

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

Для любой программы эти типы есть и дописать их можно.

Типы или классы? Речь вроде про inf / sup классы. Вот ещё одна проблема - если всё что угодно без разбора называть отношением типизации (в т.ч. отношение инстанцирования) и типами (в т.ч. классы) - получается путаница. Если говорить про хаскель, то лучше всё-таки называть типы типами, а классы классами (даже если в каком-то контексте ты можешь считать их «типами», в более общем смысле); отношение типизации - отношением типизации, а инстанцирования - инстанцированием (даже если...).

Вот мы пишем forall a. (X a, Y a) => a, тип (X a, Y a) есть? Есть. Объявлен? Нет.

Вот (X a, Y a) это не тип, это контекст (ограничение) составленное с помощью классов. Чтобы передать это ограничение аргументом конструктору типа Dynamic (из топика) его _нужно_ объявить в виде класса (класс это ограничение с именем, контекст - анонимное ограничение). Т.е. есть некая разница между _возможен_ и _существует_ (определён).

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

Хочешь сказать, что у терма all even (map (2+) [1..]) нету терма?

По-хорошему, этот терм не должен пройти проверку типов.

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

Типы или классы?

В данном случае же мы рассматриваем классы как типы (типы типов). Ну короче читай как «можно дописать классы», да.

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

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

Вот (X a, Y a) это не тип, это контекст (ограничение) составленное с помощью классов.

Ну (X a, Y a) задает универсум, по которому проводится квантификация. То есть тип, который должна иметь переменная а.

Чтобы передать это ограничение аргументом конструктору типа Dynamic (из топика) его _нужно_ объявить в виде класса

Зачем нам нужно его передавать конструктору?

Т.е. есть некая разница между _возможен_ и _существует_ (определён).

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

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

По-хорошему, этот терм не должен пройти проверку типов.

Не, ну да, в сферической в вакууме идеальной системе типов он проверку типов не проходит, и там у нас будет чистый Bool, но мы говорим о реальном тьюринг-полном ЯП с неразрешимой halting problem, а потому извольте учесть жопу.

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

В твоем понимании тогда если в ЯП есть лямбды...

Разница только в том, что в хаскеле на данный момент есть анонимные функции (лямбды) которые можно свободно использовать и нет анонимных контекстом которые можно свободно использовать и передавать куда угодно. Как в OP примере - приходится определить нужный контекст как top-level class, как если бы нужно было каждую лямбду определять отдельной top-level функцией.

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

В OP же есть пример зачем.

но это не имеет отношения к теме разговора.

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

как если бы нужно было каждую лямбду определять отдельной top-level функцией.

Ну да. Так я и говорю, по твоей логике - если в ЯП есть лямбды, то там есть все функции, а если нету лямбд - то есть только те функции, что объявлены. Это же очевидная чушь. Не говоря о том уже, что с формальной точки зрения такого понятия как «имя функции» или «имя типа» или «имя тайпкласса» вообще нету. Это ведь все объекты и стрелки, то, что мы какой-то объект/стрелку выделили и сказали «будем называть ее А» никак не соотносится с существованием этого объекта/стрелки.

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