agda или coq?

Coq лаконичней: три буквы вместо четырёх.

Даже здесь CL имеет преимущество.

> Даже здесь CL имеет преимущество.

Но даже здесь CL хуже C.

:)

Зачем?

Учи J2EE

Coq оставил отвратительное впечатление.

Сделал в нём тип векторов, параметризованных длиной. Попытался доказать простенькую теорему: вектор v длины N+1 обязательно равен cons (head v, tail v). С налёта не получилось (что уже плохой знак). Привлёк помощь друга. Мне показали гигантскую простыню, в середине которой это вроде как делается. Забил.

Agda не пробовал.

<Учи J2EE

одно другому не мешает

>Зачем?

интересно узнать, че это за языки такие, и что они умеют. интерес конечно же чисто-академический.

>Coq лаконичней: три буквы вместо четырёх.

всегда считал тебя умным и адекватным человеком. а тут - ляпнул так ляпнул.

для coq есть хороший вводный курс http://www.cis.upenn.edu/~bcpierce/sf/toc.html для agda подобного не встречал

хоть один человек ответил по теме.

>для coq есть хороший вводный курс http://www.cis.upenn.edu/~bcpierce/sf/toc.html для agda подобного не встречал

спасибо

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

>Чего на ЛОРе нет и не будет.

спорно

дак че, знакомых с агдой на лоре нет?

а то про coq ответили, и материал указали. а про агду - ноль комментов.

дак че, знакомых с агдой на лоре нет?

Будь мне надо я бы взял agda - coq это больше proof ассистент чем ЯП, а agda наоборот - сначала это ЯП, а уже потом proof ассистент. Ну и потом, agda написана на haskell - как язык она очень на haskell похожа, компилируется в haskell, реализация имеет API, FFI haskell <-> agda делается просто (см. Lemmachine - REST'ful web-сервер, написан на agda, работает поверх Hack).

а то про coq ответили, и материал указали. а про агду - ноль комментов.

Дык, в гугл. У них есть сайт, ещё видел введение тут.

> Ну и потом, agda написана на haskell - как язык она очень на haskell похожа, компилируется в haskell, реализация имеет API, FFI haskell <-> agda делается просто (см. Lemmachine - REST'ful web-сервер, написан на agda, работает поверх Hack).

а система типов там мощней чем в хаскелле?

да. скорее всего познакомлюсь с агдой.

а система типов там мощней чем в хаскелле?

Haskell98 это HM, GHC - более мощная (type checking is undecidable, type inference is impossible) вариация System F, Agda - ещё более мощные зависимые типы. При этом type checking в agde также undecidable (т.е. проверка типов может никогда не завершиться), а вот type inference совсем слабый, иначе говоря, большинство типов нужно прописывать явно (за редким исключением).

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

Ещё про отличия от coq есть тут.

>зависимые типы.

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

а вот type inference совсем слабый

ну это мы переживем

GHC - более мощная (type checking is undecidable, type inference is impossible) вариация System F

а то что сейчас в GHC, не собираются случаем перенести в следующий стандарт хацкеля? ведь как я понял, ghc - дэ-факто эталонная реализация хаскеля, не?

вот и захотел узнать, что это.

Functional dependencies и type families в GHC позволяют делать отображения «тип в тип», а с помощью кучи лишней работы механизма классов типов можно поддерживать отображения «тип в терм» и «терм в тип». Так что в GHC сейчас тоже разновидность зависимых типов, но, в отличии от agda, их очень неудобно использовать. Ну и в GHC нет indexed families, universes, implicit arguments и т.д.

не собираются случаем перенести в следующий стандарт хацкеля? ведь как я понял, ghc - дэ-факто эталонная реализация хаскеля, не?

В рамках процесса Haskell', да. Например, в стандарт Haskell 2010 уже кое-что вошло из того что было в расширениях GHC.

Так что в GHC сейчас тоже разновидность зависимых типов

Например, пишем так:

{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, FlexibleInstances, UndecidableInstances #-}

-- * Utils.

-- | Bottom value.
__ :: t
__ = __

-- | Arrow to bottom value.
___ :: a -> t
___ = const __

потом добавляем числа Пеано:

-- * Peano numbers.

infixl 6 :+
infixl 7 :*

data Z = Z
data S n = S n

-- | N : Set.
class N t where
  fromN :: t -> Integer
  toN   :: Integer -> t

-- | 0 : N.
instance N Z where
  fromN = const 0
  toN   = const Z

-- | +1 : N -> N.
instance N n => N (S n) where
  fromN = (+ 1) . fromN . p
  toN   = S . p . toN

-- | -1 : N -> N.
p :: S n -> n
p = ___ :: S n -> n

instance Show Z where 
  show = const "0"

instance N n => Show (S n) where
  show = show . fromN

-- * Functions on types.

-- | (+) : N -> N -> N
type family x :+ y :: *
type instance x :+ Z = x
type instance x :+ (S y) = S (x :+ y)

-- | (*) : N -> N -> N
type family x :* y :: *
type instance x :* Z = Z
type instance x :* (S y) = x :* y :+ x

и можно написать классический пример со списком параметризованным своей длинной:

-- * Pseudo-dep. arrays.

infixr 5 :. , ++.

data Array n a where
  E    :: Array Z a
  (:.) :: a -> Array n a -> Array (S n) a

-- | Safe `head'.
first :: Array (S n) a -> a
first (x :. _) = x

-- | Safe `tail'.
rest :: Array (S n) a -> Array n a
rest = ___

-- * Runtime length.

class Length t where
  lengthRT :: t -> Integer

instance Length (Array Z a) where
  lengthRT = const 0

instance Length (Array n a) => Length (Array (S n) a) where
  lengthRT = (+ 1) . lengthRT . rest

-- * Compile time length.

type family LengthT x :: *
type instance LengthT (Array Z a) = Z
type instance LengthT (Array (S n) a) = S (LengthT (Array n a))

lengthCT :: x -> LengthT x
lengthCT = __ :: x -> LengthT x

-- * Some functions.

(++.) :: Array n a -> Array m a -> Array (m :+ n) a
E         ++. ys = ys
(x :. xs) ++. ys = x :. xs ++. ys

afoldr :: (a -> b -> b) -> b -> Array n a -> b
afoldr _ z E         = z
afoldr f z (x :. xs) = f x $ afoldr f z xs

afoldl :: (a -> b -> a) -> a -> Array n b -> a
afoldl _ z E         = z
afoldl f z (x :. xs) = afoldl f (f z x) xs

amap :: (a -> b) -> Array n a -> Array n b
amap _ E         = E
amap f (x :. xs) = f x :. amap f xs

class Replicate n where
  areplicate :: n -> a -> Array n a

instance Replicate Z where
  areplicate Z _ = E

instance Replicate n => Replicate (S n) where
  areplicate (S n) x = x :. areplicate n x

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