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

Crossposts: http://stdray.livejournal.com/74702.html

Entry tags:

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

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

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

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

Threaded | Top-Level Comments Only

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

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

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

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

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

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

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

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

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

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

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

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

{-# 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 (+)

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

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

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

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

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

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

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

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

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

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

Edited 2012-10-18 16:05 (UTC)

Threaded | Top-Level Comments Only

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

no subject

no subject

no subject

no subject

no subject

no subject

no subject

no subject

no subject

no subject