Об отсутствии кота

вообще норма, а не исключение.

Елена, залогиньтесь.

обычно сторонники динамической типизации как раз понимают статику лучше

не замечал

в хаскикомьюнити

это всё следствие успешности языка. посмотри на агдакомьюнити

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

Вообще, строго говоря, статическая типизация, сама по себе, ничем не тличается от динамической, с точки зрения семантики. Отличие чисто техническое: ошибки (типов) в динамической, вскрываются в рантайме (или вообще не вскрываются). Тут путаница идет в терминологии. На самом деле, речь обычно идет о явной/неявной и строгой/нестрогой. Именно это следовало бы обсуждать. А тут целый тред ни о чем.

И вообще пишешь идеальный код без ошибок.

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

Только в каком-нибудь C++98.

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

Третья Теорема Лавсана

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

Вообще, строго говоря, статическая типизация, сама по себе, ничем не тличается от динамической, с точки зрения семантики.

Осиль хотя бы введение к TAPL.

«Что и требовалось доказать» где?

не замечал

Плохо смотрел.

это всё следствие успешности языка. посмотри на агдакомьюнити

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

Нех*я ничего осиливать. Ты споришь с прописной истиной. В сраном хаскеле строгая явная типизация. Ты вообще, видать, не понимаешь, что такое типы в языках.

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

Но ты не сможешь его заставить пользоваться «подстеленными» вещами. Он сделает work-around, потому что «так на 3.5 сточки короче» и по пизде пойдут твои соломоподстилки. Или вообще не будут использовать твою библиотеку.

Плохо смотрел

огорчение-то какое

дизайн хаскеля предполагает использовать статику _как можно меньше_

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

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

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

особенно вредно доверять в этом вопросе языкам программирования

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

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

if true than
ok
else
bad_typed_term

, коль семантика одинакова.

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

или думать головой. что я, собственно, и предлагаю

выбрать язык

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

Так я написал об этом, разуй глаза. Но к семантике это отношения не имеет, грамотей.

или думать головой. что я, собственно, и предлагаю

При чем тут «думать»?

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

А я о чем?

Так ты какую семантику имеешь в виду? Денотационную, операционную или, может, аксиоматическую?

А я о чем?

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

При чем тут «думать»?

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

Третья Теорема Лавсана (о бесполезности статической типизации)

О, ЧСВ как раздуло у борщевичка

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

Я говорю - к чему ты это упомянул? Как польза мышления связана с тем, что в языке Х удобно/легко писать говнокод и нудобно/сложно писать хороший код?

о том, какой плохой язык Haskell

Да нет, я не о том. Я о том, что хаскель спроектирован так, что типизацию использовать неудобно. И ее никто не использует.

И ее никто не использует.

И ты тут такой с пруфами, что _никто_ её не использует.

метапрограмированием

Ортогонально же, нет?

хаскель спроектирован так, что типизацию использовать неудобно

а какой язык спроектирован так, что типизацию использовать удобно?

Как польза мышления связана с тем, что в языке Х удобно/легко писать говнокод и нудобно/сложно писать хороший код?

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

Жирновато.

И ты тут такой с пруфами, что _никто_ её не использует.

Ну может 3.5 человека и использует - но это совершенно редкое исключение из правил.

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

Готов спорить, что это динамический рэкетир :)

а какой язык спроектирован так, что типизацию использовать удобно?

Я такого не знаю. Но это не значит, что подобного языка нет (и тем более, что он невозможен).

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

И какое высказывание излишне общно?

Что-то ты быстро сдулся. Так не весело.

какое высказывание излишне общно?

в языке Х удобно/легко писать говнокод и нудобно/сложно писать хороший код

там как бы неявный forall в утверждении, а так не бывает (кроме случая PHP)

Где неявный forall?

Не вижу, где я сдулся.

Где неявный forall?

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

Ты можешь переписать мое утверждение, доставив этот предполагаемый forall явно?

Он же лиспер. Им такие понятия неведомы.

Ну, смотри. Статическая типизация это всего лишь крохотное подмножество compile-time метапрограммирования. Вернее, было бы, если бы алгоритм тайпчека можно было бы менять используя сам язык.

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

Об отсутствии кота (комментарий)

исчерпывающе.

Ах ты пьяная скотина...

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

От нас не убежит, блеать!

Вот ето слив.

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

{-# LANGUAGE TypeOperators, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, IncoherentInstances #-}
module Main where

data Expr f = In (f (Expr f ))

data (f :+: g) e = Inl (f e) | Inr (g e)

instance (Functor f , Functor g) => Functor (f :+: g) where
	fmap f (Inl e1 ) = Inl (fmap f e1 )
	fmap f (Inr e2 ) = Inr (fmap f e2 )

class (Functor sub, Functor sup) => sub :<: sup where
	inj :: sub a -> sup a

instance Functor f => f :<: f where
	inj = id
instance (Functor f, Functor g) => f :<: (f :+: g) where
	inj = Inl
instance (Functor f, Functor g, Functor h, f :<: g) => f :<: (h :+: g) where
	inj = Inr . inj

inject :: (g :<: f) => g (Expr f) -> Expr f
inject = In . inj

class Render f where
	render :: Render g => f (Expr g) -> String

instance (Render f, Render g) => Render (f :+: g) where
	render (Inl x ) = render x
	render (Inr y) = render y

pretty :: Render f => Expr f -> String
pretty (In t) = render t




data CatName e = CatName String
data CatHeight e = CatHeight Float

data Cons e = Cons e e

instance Functor CatName where
	fmap f (CatName x) = CatName x
instance Functor CatHeight where
	fmap f (CatHeight x) = CatHeight x

instance Functor Cons where
	fmap f (Cons e1 e2) = Cons (f e1) (f e2)


catName :: (CatName :<: f) => String -> Expr f
catName x = inject (CatName x)

catHeight :: (CatHeight :<: f) => Float -> Expr f
catHeight x = inject (CatHeight x)

(|:|) :: (Cons :<: f) => Expr f -> Expr f -> Expr f
x |:| y = inject (Cons x y)



instance Render CatName where
	render (CatName i) = show i

instance Render CatHeight where
	render (CatHeight i) = show i

instance Render Cons where
	render (Cons x y) = "(" ++ pretty x ++ " . " ++ pretty y ++ ")"


-- Итак... 
-- Просто кот
a :: Expr (CatName) 
a = catName "foo"

-- Коробка с двумя котами
b :: Expr (Cons :+: CatName)
b = catName "foo" |:| catName "boo"


-- Коробка с двумя принципильно разными котами, не компилируется
c :: Expr (Cons :+: CatHeight :+: CatName)
c = catHeight 0.2  |:| catName "foo"

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

Палю: все крохотное подмножество метапрограммирования.

маразм какой-то, ниже и то оверкил, т.к. под задачу в вакууме

{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}

data CB :: [*] -> * where
  Z :: CB '[]
  O :: a -> CB '[a]
  D :: a -> CB c -> CB (a ': c)

cbHead :: CB (a ': b) -> a
cbHead (O a) = a
cbHead (D a _) = a

cbTail :: CB (a ': b) -> CB b
cbTail (O a) = Z
cbTail (D _ t) = t

class HaveName a where getName :: a -> String
class HaveHeight a where getHeight :: a -> Int

data CN = CN String deriving (Show)
instance HaveName CN where getName (CN n) = n
data CNH = CNH String Int deriving (Show)
instance HaveName CNH where getName (CNH n _) = n
instance HaveHeight CNH where getHeight (CNH _ h) = h

test = D (CN "Vasya") (O (CNH "Kuzya " 5))

*Main> :t test
test :: CB '[CN, CNH]
*Main> cbHead test
CN "Vasya"
*Main> cbHead (cbTail test)
CNH "Kuzya " 5

для тех кто любит операторы:

(->|) :: a -> CB b -> CB (a ': b)
a ->| Z = O a
a ->|  b  = D a b
infixr 5 ->|

test = (CN "Vasya") ->| (CNH "Kuzya " 5) ->| Z

Спали уже свои источники, где так научился? Я тоже хочу.

на работе, проект где немного такой магии нужно было попался и сотрудники, которые умеют :P.

Вообще в haskell-cafe всяких интересных штук для работы с типами проскативает, причем моих скилов далеко не всегда хватает на их быстрое осознание.

P.S. вообще непорядок, обычно на лоре меня некомпетентным идиотом называют, а не источники спрашивают :)

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

Только в каком-нибудь C++98.

Да и там не очень, тайпдефами можно забороть.

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

data CatProps :: * -> * where
  CatName :: CatProps String
  CatHeight :: CatProps Int

-- бойлерплейт, который сгенерится TH или руками
 
vasya = DM.fromList [CatName :=> "Vasya"]
kuzya = DM.fromList [CatName :=> "Kuzya" , CatHeight :=> 5]

*Main> let t = vasya ->| kuzya ->| Z
*Main> (cbHead t) ! CatName
"Vasya"
*Main> CatHeight `DM.lookup` cbHead t
Nothing
*Main> CatHeight `DM.lookup` cbHead (cbTail t)
Just 5

Поддтипирование можно делать через

data SubCat :: * -> * where
  CatSurname :: SubCat String
  SubCat     :: SubCat (DM.DMap CatProps)

Хотя это и не идеальный вариант.

Но в обычном коде можно следовать KISS и не выпендриваться.

P.S. открытые множется без поддтипирования оставляю

lisp:

(cons cat (cons other-cat nil))

{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}

data CB :: [*] -> * where
  Z :: CB '[]
  O :: a -> CB '[a]
  D :: a -> CB c -> CB (a ': c)

cbHead :: CB (a ': b) -> a
cbHead (O a) = a
cbHead (D a _) = a

cbTail :: CB (a ': b) -> CB b
cbTail (O a) = Z
cbTail (D _ t) = t

class HaveName a where getName :: a -> String
class HaveHeight a where getHeight :: a -> Int

data CN = CN String deriving (Show)
instance HaveName CN where getName (CN n) = n
data CNH = CNH String Int deriving (Show)
instance HaveName CNH where getName (CNH n _) = n
instance HaveHeight CNH where getHeight (CNH _ h) = h

test = D (CN "Vasya") (O (CNH "Kuzya " 5))

няня я у них поел