очень плохая ссылка

[stdray]

про мифический хаскель (линк).

Блин, аж до тошноты. Атд есть динамическая типизация. Типы нужны, чтобы узнать какое количество памяти надо выделить. Метки типов. Типов пустых туплов. Классы типов — это АлгТД. Классы типов - недокостыль. Система типов — это лишь инструмент для разметки памяти под данные и связи кода с данными. Статическая типизация: это когда в исходнике if есть (в том или ином виде: ПМ, overloading и т.д.), а в генеренном коде if-а нет? Боксирование...

Как всякие морготные фильмы ужасов. Когда кровь, кишки, слизь какая-то, глаз выпал, и кто-то постоянно нападает из-за угла. Смотреть противно, но все равно смотришь. Даже не уверен, что мне интересен конец истории. Смотришь и плющит. Эмоции как-никак, хоть и негативные.

Comments

[wizzard]

ну дык, если рассматривать хаскель на уровне рантайма, то так оно примерно и есть...

и метапрограммированием можно много где заниматься, хоть на ассемблере (в смысле self-modifying code)

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

[stdray.livejournal.com]

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

[thesz.livejournal.com]

Насчёт "типов нет" я бы не был так уверен: http://www.crash-safe.org/ (а до этого тоже хватало, i432, например).

[isorecursive.livejournal.com]

> Атд есть динамическая типизация.
Согласен. И на физическом, и на концептуальном уровне.
Вот такое соответствие:
Алгебраический тип <-> Система типов динамического языка
Конструктор алгебраического типа <-> Тип в динамическом языке
Паттерн-матчинг конструктора <-> Динамическая диспатчеризация по типу

Остальное - что-то странное, но по ссылке идти вчитываться настроения нет.

[stdray.livejournal.com]

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

 
int x = ...
switch(x){
     case 0: ....
     case 1: ....
     case 2: ....
}

тоже имеет какое-то отношение к динамической типизации?

[isorecursive.livejournal.com]

> тоже имеет какое-то отношение к динамической типизации?
Маленькое. Аналогия для физического соответствия следует из этой:
Конструктор алгебраического типа <-> Тип в динамическом языке
И она такая:
Рантаймая информация о конструкторе <-> Рантаймовая информация о типе

> При этом есть критерии, как их всех между собой различать.
Не на уровне типов в понимании последних с точки зрения статической типизации.
Может так понятнее будет:

{-# LANGUAGE NoMonomorphismRestriction, NoImplicitPrelude, Rank2Types, UnicodeSyntax, LambdaCase, RebindableSyntax, OverloadedStrings #-}
module DynamicTyping where

import qualified Prelude as P
import Prelude hiding ((+), (-), (*), error, fromInteger, fromRational) -- (Num, Show, Read, show, (.), (>>))
import Prelude.Unicode

fi = P.fromIntegral

-- our tiny dynamic type system
data T = IntT Integer
       | FloT Float
       | StrT String
       | FunT (T → T)

instance Show T where
  show = \case
    IntT x → show x
    FloT x → show x
    StrT x → x
    FunT x → show "#"

error ∷ T → a
error s = P.error (show s)

arithT ∷ (∀ a. Num a ⇒ a → a → a) → T → T → T

arithT o (IntT x) (IntT y) = IntT (fi x `o` fi y)
arithT o (IntT x) (FloT y) = FloT (fi x `o` y   )
arithT o (FloT x) (IntT y) = FloT (x    `o` fi y)
arithT o (FloT x) (FloT y) = FloT (x    `o` y   )
arithT _ _        _        = error "Incompatible types!"

(+), (*), (-), (@@) ∷ T → T → T

(+) = arithT (P.+)
(*) = arithT (P.*)
(-) = arithT (P.-)

x @@ y = StrT (show x P.++ show y)

-- here we throw away haskell types,
--   downshifting values to embedded dynamic subworld of T
fromInteger  = IntT
fromRational = FloT ∘ P.fromRational
fromString   = StrT

x ∷ T
x = 32 + 1.213 @@ " i'm so dynamic " @@ 12.345

y ∷ T
y = 1 + "typechecks perfectly…"

say x = P.putStrLn (show x)

main = say x >> say y
-- > 33.213 i'm so dynamic 12.345
-- > Exception: Incompatible types!

-- we can even throw away haskell arrows,
--   downshifting binary functions on downshifted values to embedded dynamic subworld of T
downshift ∷ (T → T → T) → T
downshift f = FunT (\x → FunT (f x))

(+%) ∷ T
(+%) = downshift (+)

[stdray.livejournal.com]

>Не на уровне типов в понимании последних с точки зрения статической типизации.

Я не говорил, что ветки атд различимы на уровне типизации. Я как раз говорил, что это один тип, который известен на этапе копиляции. Хотя, конечно, матч по атд похож на динамическое "посмотреть метку типа лежащую рядом с указателем", это принципиально разные вещи, на мой взгляд. То есть как оно там будет реализовано, никого не волнует. Вопрос, что мы знаем в compile time. В случае с атд знаем про сам тип, а так же тип функций-конструкторов. В случае с динамикой, такой информации нет. А уж какая там ветка сопоставится, имхо, такого же уровня вопрос, как в случае с сопоставление элементарных типов (интов каких или булов), но для них почему-то никакой речи о динамической типизации не идет.

[isorecursive.livejournal.com]

> Вопрос, что мы знаем в compile time. В случае с атд знаем про сам тип, а так же тип функций-конструкторов. В случае с динамикой, такой информации нет.
Почему же нет? Можно представить, что в динамике у нас в компайл-тайме достоверно известно: все термы одного и того же типа - одного из таких вот Т, которые мы можем объявлять в хаскеле показанным выше образом. А типы конструкторов можно вывести из стандарта данного динамического языка (они там будут называться "элементарные типы" и "определённые пользователем типы" и прочее в таком духе).

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

> это принципиально разные вещи, на мой взгляд
Наверное, соответствия Карри-Говарда тебе тоже не понравятся.

[stdray.livejournal.com]

>Можно представить, что в динамике у нас в компайл-тайме достоверно известно: все термы одного и того же типа
Согласен. (1)

>А типы конструкторов можно вывести из стандарта данного динамического языка
Можно. Статический анализ никто не отменял. Но по факту, динамика на то и динамика, что в компайл-тайм ничего подобного не известно.

>Не понял, о чём речь.
Я просто провел аналогию, что есть тип и его значения мы можем как-то различать. В одном случае (атд) говорят о динамической типизации, в другом (инт, бул) - просто про условный оператор.

>Наверное, соответствия Карри-Говарда тебе тоже не понравятся.
Я его не до конца понимаю, потому не могу говорить, нравится мне или нет, как не очень понимаю, какое отношение он имеет к обсуждаемому вопросу. Там что-то про типы и доказательство их существования. Если трактовать динамику описанным выше образом (см. 1), мы каждый раз будем доказывать (или не доказывать, что являет собой какие-то взаимоисключающие параграфы), что ентот единственный тип не пуст. Мне это не кажется хоть сколько-нибудь интересным. Хотя, опять же, у меня нет пониманию, потому, может, я бред несу.

[isorecursive.livejournal.com]

> не очень понимаю, какое отношение он имеет к обсуждаемому вопросу
Там соответствия более дерзкие, и менее очевидные:
Тип <->Теорема
Терм типа <-> Доказательство
Функция <-> Импликация
Аппликация функции <-> Модус поненс
Логическое И <-> Тупл
Логическое ИЛИ <-> Either
> мы каждый раз будем доказывать, что ента единственная бессмысленная теорема верна. Мне это не кажется хоть сколько-нибудь интересным.
Да, именно поэтому никто и не использует динамическую типизацию для этих вещей.