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]
★★★★

Суперкомпиляцию уже запилили? А то Пейтон-Джонс как к нам на конфу съездил, так загорелся желанием. И да, Хаскель скоро лопнет от сущностей и фич.

buddhist ★★★★★
()

А зачем ShowShapeInterface класс? Можно ведь

type ShowShapeInterface t = (Show t, ShapeInterface t)

Так?

И вообще, хочется сразу написать

type Shape = Dynamic (Show t, ShapeInterface t)
Без лишних типов.

-XPolyKinds не очень много меняет - просто позволяет писать чуть более строго типизированный type-level код

С нетипизированого до типизированого — это, по-моему, чуть более, чем «чуть более».

P.S.: дожили, примеры на геометрических примитивах в хаскеле. Что дальше, факториалы в С++?

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

Суперкомпиляцию уже запилили?

Есть бранч, но там последний коммит был в сентябре прошлого года. С другой стороны, там делается именно с помощью compiler plugin-а (адаптируется код из CHSC), так что это уже не вопрос GHC, а вопрос реализации пригодной для больших программ суперкомпиляции System F. Любую такую реализацию можно адаптировать для GHC как core-to-core плагин.

quasimoto ★★★★
() автор топика

теперь можно проводить forall квантификацию не только по типам (:: *), но и по классам типов (:: Constraint).

Еще немного - и можно будет даже написать map для гетерогенных списков!

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

Так?

Нет. type определяет тип (:: *), а конструктор типа Dynamic принимает первым аргументом одно-параметрический класс типов (:: * -> Constraint). И само выражение type ShowShapeInterface t = (Show t, ShapeInterface t) не имеет смысла - ShowShapeInterface :: * -> * (тип-в-тип), но Show :: * -> Constraint (тип-в-класс), ShapeInterface :: * -> Constraint (тоже), (,) :: * -> * -> * (тип-в-тип-в-тип). Получается ill-typed.

И вообще, хочется сразу написать

А вот это уже может иметь смысл (но сейчас так нельзя - получается «predicate used as a type») - компилятор, во-первых, должен вывести из того что Show :: * -> Constraint и ShapeInterface :: * -> Constraint, то что (Show t, ShapeInterface t) :: * -> Constraint, и он подходит по kind-у для Dynamic, во-вторых, он должен уметь применить cls = (Show t, ShapeInterface t) :: * -> Constraint в выражении forall cls a. cls a => a, так чтобы (Show t, ShapeInterface t) a => (Show a, ShapeInterface a), ну и вообще уметь квантифицировать по таким сложным (как они фигурируют в контекстах) классам.

С нетипизированого до типизированого — это, по-моему, чуть более, чем «чуть более».

Может быть. Просто type-level находит не очень широкое применение пока - ну сможем мы сделать более чёткий Vector параметризованный type-level числами. Хорошо конечно.

дожили, примеры на геометрических примитивах в хаскеле. Что дальше, факториалы в С++?

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

С constraint kinds фича в том, что будет одна динамическая обвёртка на все интерфейсы и типы (с existential quantification - столько, сколько интерфейсов и их комбинаций).

quasimoto ★★★★
() автор топика

Если все типы объединяются в kind *, то все классы типов объединяются в kind Constraint

Наверное правильнее будет «kind Constraint - все типы, являющиеся инстансами некоторого тайпкласса»?

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

Наверное правильнее будет «kind Constraint - все типы, являющиеся инстансами некоторого тайпкласса»?

вроде того

Int :: *
Num :: * -> Constraint
Num Int :: Constraint
Monad :: (* -> *) -> Constraint
Monad IO :: Constraint
* :: BOX
Constraint :: BOX

Int, IO - types, Num, Monad - typeclasses, *, Constraint - kinds, BOX - sort.

quasimoto ★★★★
() автор топика

позднее связывание

В каком смысле - композиция через произвольный тип с зафиксированным классом в контексте не является идиомой (вроде show . read), в этом смысле у методов нет динамической диспетчеризации из коробки (как в CLOS, в хаскеле всегда подставляется спецификация метода во время компиляции). Но композиция через «динамический» (existential \ GADT, вроде area . circle) - обычная композиция и может служить для реализации позднего связывания. Например:

readShape :: IO (Maybe Shape)
readShape = do
  shape <- putStrLn "shape?" >> getLine
  case shape of
    "square" -> putStrLn "side?" >> fmap read getLine >>= return . Just . square
    "circle" -> putStrLn "radius?" >> fmap read getLine >>= return . Just . circle
    _ -> putStrLn "unknown shape" >> return Nothing

performMethod :: Shape -> IO ()
performMethod shape = do
  method <- putStrLn "method?" >> getLine
  case method of
    "area" -> putStrLn $ show $ area shape
    "perimeter" -> putStrLn $ show $ perimeter shape
    _ -> putStrLn "unknown method"

io :: IO ()
io = forever $ do
  s <- readShape
  case s of
    Just s' -> performMethod s'
    Nothing -> return ()

-- > io
-- shape?
-- circle
-- radius?
-- 5
-- method?
-- area
-- 78.53981633974483
-- shape?
-- square
-- side?
-- 6
-- method?
-- perimeter
-- 24.0

Тут одна функция возвращает Shape (динамический тип) в IO (во время компиляции точно нельзя сказать что там будет), а другая вызывает метод на Shape - выбор конкретного метода для square / circle происходит во время выполнения.

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

так ведь не работает :(

Prelude> map show [1,"2"]

<interactive>:1:10:
    No instance for (Num [Char])
      arising from the literal `1' at <interactive>:1:10
    Possible fix: add an instance declaration for (Num [Char])
    In the expression: 1
    In the second argument of `map', namely `[1, "2"]'
    In the expression: map show [1, "2"]
Prelude>

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

так ведь не работает :(

Обсуждали уже. Но это в контексте топика.

Old way:

-- * Take 1.

data Dyn = forall a. Dyn a

-- > map show [Dyn 1, Dyn "2"]
-- No instance for (Show Dyn)

-- * Take 2.

data Dyn = forall a. Show a => Dyn a

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

-- > map show [Dyn 1, Dyn "2"]
-- ["1","\"2\""]

New way:

data Dynamic :: (* -> Constraint) -> * where
  Dynamic :: forall cls a. cls a => a -> Dynamic cls

-- > map show ([Dynamic 1, Dynamic "2"] :: [Dynamic Show])
-- No instance for (Show (Dynamic Show))

-- So,

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

-- > map show ([Dynamic 1, Dynamic "2"] :: [Dynamic Show])
-- ["1","\"2\""]

Т.е. больше не надо паковать контексты в existential типы (раньше именно это всё портило). Правда, есть два момента. Чтобы поднять для Dynamic сразу много интерфейсов нужно их сложить:

class (X1 t, X2 t, ..., Xn t) => Sum t
instance (X1 t, X2 t, ..., Xn t) => Sum t

если бы был class-level с class-абстракциями и -аппликациями, то можно бы было просто отдавать Dynamic абстракцию - (X1 t, X2 t, ..., Xn t), или что-то более сложное (?a b -> X a b, Y b a, ...).

Второй момент - нужен набор Dynamic, Dynamic2, Dynamic3, ... для одно-, двух-, трёх- и т.д. параметричных классов типов.

Что касается map для типов-произведений - (,) :: * -> * -> *, (,) :: forall a b. a -> b -> (a, b), то я вообще не могу их представить в свете вот этого:

(\f (x, y) -> (f x, f y)) id (1, "2")
quasimoto ★★★★
() автор топика
Ответ на: комментарий от quasimoto

Old way:

Old way никакого не было как раз, т.к. приходилось писать свой map для каждого набора тайпклассов.

Т.е. больше не надо паковать контексты в existential типы (раньше именно это всё портило).

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

(\f (x, y) -> (f x, f y)) id (1, «2»)

Надо же (\f (x, y) -> (f x, f y)) id (Dynamic 1, Dynamic «2»)

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

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

Квантификация всегда подразумевает универсум по которому она и производится (тут - kind-ы).

Надо же (\f (x, y) -> (f x, f y)) id (Dynamic 1, Dynamic «2»)

Ну да. Я про то что map для настоящих гетерогенных коллекций (таких как tuple) я нигде не видел - в hlist, например, она тоже не умеет полиморфных и перегруженных функций.

quasimoto ★★★★
() автор топика

— Компактность и ортогональность!

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

anonymous
()

я поражаюсь сколькому ещё всему надо научиться.. (мне)

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

Квантификация всегда подразумевает универсум по которому она и производится (тут - kind-ы).

Ну вот в том и проблема - у нас была квантификация по *, ввели квантификацию по Constraint < *, а нужна квантификация по * -> Constraint, то есть по тайпклассу. Сейчас мы можем писать forall cls a . (cls a) => a, где cls - тайпкласс, а надо уметь просто forall cls . (cls a) => a, где cls - тайпкласс. То есть полноценный полиморфизм на уровне типов, соответственно и forall должен иметь другуя семантику - универсум обычного forall это типы, универсум нужного forall - типы типов.

anonymous
()

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

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

Почему передумал? Как сказал - так и сделал «кое-что».

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

само выражение type ShowShapeInterface t = (Show t, ShapeInterface t) не имеет смысла

Вру. Судя по докам так можно написать, только это не синоним типа, это синоним класса (не стали вводить новое ключевое слово - data newtype / type ~ class / эта вещь). Но всё равно он тут не применяется - нужно полное объявление класса, а не его синоним (как обычно бывает с newtype / type).

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

нужна квантификация по * -> Constraint

Именно по этому и идёт квантификация сейчас. (forall cls a. cls a => a) тут cls :: * -> Constraint. Аналогично, (forall cls a b. cls a b => a -> b), cls :: * -> * -> Constraint. И т.п.

(cls a =>) тут похож на implicit argument из agda.

Квантификация просто по Constraint это вообще странно (по всем ограниченным типам что ли?).

а надо уметь просто forall cls . (cls a) => a

Не понял - это type scheme по a, раскрывается в (forall cls. (forall a. cls a => a)), т.е. нужно чтобы были разные forall - отдельно для классов и отдельно для типов? Ну сейчас так и есть - (forall cls a. cls a => a) это, считай, и есть короткая форма этого (forallClass cls. (forallType a. cls a => a)), т.к. как компилятор знает, что cls это constraint, а `a' - тип. Просто с точки зрения синтаксиса языка такие разные forall не нужны (с ними нечего делать).

универсум нужного forall - типы типов.

Типы типов не имеют отношения к constrained type. В хаскеле типов типов вообще нет (нет иерархии универсумов в духе MLTT).

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

И после этого говорят, что Scala переусложнена?

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

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

К счастью, пока с таким не сталкивался :) В крайних случаях спасают AnyRef и Any, как и в остальных мейнстримных языках. Просто не стоит пытаться все свести к статической типизации, чем грешат, кстати, в Хаскеле, и тогда очень многое можно удачно запрограммировать, прибегнув где нужно к динамике. Все время приходится чем-то жертвовать.

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

По-моему здорово подливает масла в огонь переусложненности Скалы ее библиотека коллекций. На мой взгляд было бы меньше проблем, если бы методы вынесли в отдельные объекты-компаньоны. Получилось бы что-то типа модулей List и Seq из F#. Дешево и сердито. Зато всем понятно что к чему. А так даже меня, очень терпеливого на этот счет человека, задалбывает разбираться во всей этой иерархии типажей и классов из библиотеки коллекций.

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

В хаскеле типов типов вообще нет

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

(forall cls a. cls a => a) это, считай, и есть короткая форма этого (forallClass cls. (forallType a. cls a => a))

Может, я что-то не так понял. Вот так можно написать: map :: forall cls. forall b. (forall a. (cls a) => a -> b) -> [forall a. (cls a) => Box a] -> b?

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

Из «Практики функционального программирования»:

— Насколько я понимаю, две активных области исследований сейчас — Data Parallel Haskell и суперкомпиляция.

Саймон: Я только что вернулся из России, с конференции Meta 2010, которая была во многом посвящена суперкомпиляции. Сейчас эта тема меня особенно интересует. Эта технология компиляции существует уже давно. Ее создал русский ученый, Валентин Турчин. Он выразил ее в терминах своего языка РЕФАЛ, о котором больше никому не было известно. Лишь позднее Роберт Глюк (Robert Glück) и его студент Мортен Соренсен (Morten Sørensen) объяснили суперкомпиляцию более понятно для остальных. Но и это было достаточно давно. Я недоумевал, почему никто не применяет суперкомпиляцию для построения настоящих оптимизирующих компиляторов? Теперь я кое-что понимаю! На первый взгляд кажется, что эту технологию можно просто реализовать по статье, но на самом деле там много «ручек». Нужно принять много архитектурных решений. И неочевидно, какие именно решения надо принять.

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

И да, Хаскель скоро лопнет от сущностей и фич.

С чего бы, Haskell2010 - 120 страниц, если не учитывать библиотеки. Или пишем хаскель, подразумеваем ghc? Расширений там много, но большинство все же костыли.

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

Ну да, в настоящее время все больше Haskell == GHC. Другой нормальной реализации нет. NHC еле шевелится, Hugs тоже.

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

Не обращай внимания, аноним херню спорол.

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

Тип типов — это каинд.

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

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

Тайпкласс - это и есть тип типов.

Тип типов это U₀, тип типов типов - U₁, и т.п. U₀ это универсум обычных (малых) типов и функций, U₁ _можно использовать_ как универсум для обобщённых (generic) типов и функций. Но это имеет малое отношение к constrained types.

Тайпкласс это сам по себе некий костыль, поэтому ставить равенство между Constraint и Type (U₀) я бы не стал, даже не стал бы ставит знак включения Constraint в Type.

В Agda, например, нет никакой сущности «класс типов», для интерфейсов используются обычные inductive families - Eq, Functor это обычные типы, при этом Eq помещается в Set (U₀), Functor может как не поместиться (будет в Set₁, т.е. U₁), так и поместиться (с помощью universe polymorphism). Так как они обычные типы - агрегация интерфейсов и теорем про интерфейсы производится как обычная агрегация типов. Ad-hoc полиморфизм сейчас (2.3.0) появился в виде instance arguments.

На эту тему есть «On the Bright Side of Type Classes: Instance Arguments in Agda», там обсуждается Haskell, Scala и Agda.

Вот так можно написать

$ ghci-7.4.0.20111219 -XRankNTypes -XKindSignatures -XConstraintKinds -XImpredicativeTypes
Prelude> data Box :: * -> *
Prelude> let map = undefined :: forall cls. forall b. (forall a. (cls a) => a -> b) -> [forall a. (cls a) => Box a] -> b
Prelude> :t map
map
  :: (forall a. (cls a) => a -> b)
     -> [forall a. (cls a) => Box a] -> b
Prelude>
quasimoto ★★★★
() автор топика
Ответ на: комментарий от anonymous

Аналог обычной типизации на уровне типов - это именно тайпклассы.

«Обычная типизация на типах» это MLTT / CoC.

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

Что выразительнее --- типы в GHC с костылями или система типов агды?

GHC начинался как HM, потом перешёл на System F, потом там появились разные расширения. Agda это настоящая реализация MLTT со своими расширениями, она всяко выразительнее.

Но при этом agda _не_ тьюринг-полная.

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

U₁ _можно использовать_ как универсум для обобщённых (generic) типов и функций.

Обобщенные типы и функции - это нетипизированная лямбда, типов там нет.

Тайпкласс это сам по себе некий костыль, поэтому ставить равенство между Constraint и Type (U₀) я бы не стал, даже не стал бы ставит знак включения Constraint в Type.

А кто ставит равенство? Просто тайпклассы - это типы типов. При чем тут Constraint?

В Agda, например, нет никакой сущности «класс типов», для интерфейсов используются обычные inductive families - Eq, Functor это обычные типы, при этом Eq помещается в Set (U₀), Functor может как не поместиться (будет в Set₁, т.е. U₁), так и поместиться (с помощью universe polymorphism).

А при чем тут агда? Меня просто поражает твое умение говорить не по делу :)

Вот у нас есть обычное лямбда-исчисление, теперь мы добавили типы и можем вводить ограничения на аргументы/результат ф-й, теперь добавили полиморфизм, а полиморфная ф-я есть ни что иное, как ф-я из множества типов в множество функций. ограничений нет - соответственно, мы получили аналог обычной лямбды на уровне типов. Если у нас есть тайпклассы, то мы эти ограничения можем устанавливать в точности так же, как и для обычных ф-й - то тайпклассы это типы типов, каждый тип принадлежит набору тайпклассов. Ну а если мы умеем квантификацию по тайпклассам - то получаем полиморфную типизированную лямбду на уровне типов. Так понятно? Как там что называется - это вообще чепуха, это не важно. Важно, чем объекты являются де-факто.

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

Но при этом agda _не_ тьюринг-полная.

Ну и что, собственно? Разве это ограничивает алгоритмическую выразительность агды по сравнению с тьюринг-полным ЯП _на практике_? Нет :)

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

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

Просто тайпклассы - это типы типов.

0 :: Int, не существует такого t != Int, что 0 :: t. Аналогично для любого конструктора - Con ... :: Type, не существует такого t != Type, что Con ... :: t. В этом смысл понятия «типизация» - у каждого терма один и только один тип. При этом у типа может быть от нуля и более инстансов - Int is instance of Num, Int is instance of Eq, etc. Т.е. типы и классы типов не составляют отношения типизации, чтобы можно было говорить «классы типов это типы типов».

А при чем тут агда?

Это область известного, MLTT (там всё типизировано - U₀, U₁, ... нет никаких «нетипизированных лямбд»). То о чём ты рассуждаешь - интуиция может подсказывать такие аналогии, но при этом она может и подвести, хочется оперировать общепринятыми чётко очерченными понятиями.

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

Ну и что, собственно?

Ничего, просто констатирую факт.

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

Там еще вывода типов нет.

Какой-то есть (например для CAFs - foo = ...). В остальном его нет даже не столько из-за зависимых типов, сколько из-за того, что нет naming convention для конструкторов, сами конструкторы перегружены, и нет схем типов (при использовании неизвестного параметра в типе он не относится к Set по умолчанию).

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

сами конструкторы перегружены, и нет схем типов

С другой стороны, а нужен ли он вообще? В том же хаскеле в определенных ситуациях он все-равно не работает. А еще чаще является причиной феерических сообщений об ошибках.

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

В этом смысл понятия «типизация» - у каждого терма один и только один тип.

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

При этом у типа может быть от нуля и более инстансов - Int is instance of Num, Int is instance of Eq, etc.

Ну да - каждый тип может принадлежать к любому количеству типов типов.

То о чём ты рассуждаешь - интуиция может подсказывать такие аналогии

При чем тут аналогии? Есть формально строгие математические определения. Если объект удовлетворяет определению Х, то объект есть Х.

хочется оперировать общепринятыми чётко очерченными понятиями.

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

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

С другой стороны, а нужен ли он вообще?

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

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

а нужен ли он вообще?

Для top-level функций может и нет - документация, контракт. Но для локальных и анонимных функций - писать ... myData ... where myData :: Data; myData = ... тип для вполне конкретной функции myData, или, наоборот, писать (\(x :: forall a. a) (xs :: forall a. [a]) -> ...) для вполне полиморфной функции, - слишком вербозно.

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