IO -- это монада IO -- это функтор IO -- это конструктор типа Петя -- человек Петя -- хаскеллист Петя -- спамер

человек не является понятием человека

поэтому IO является монадой, но не является Monad

человек не является понятием человека

а трубка?

нет. везде существительное

И тогда где тут тайпкласс? Тайпкласс это свойство же

С этим к Евгению, он-то утверждает, что монада - это свойство, а поэтому являться монадой ничего не может

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

IO is a monad, but not the Monad

IO -- это монада IO -- это функтор IO -- это конструктор типа Петя -- человек Петя -- хаскеллист Петя -- спамер

нет, нет, да

каждый хаскелист - человек, но не каждый человек хаскелист

да нет, это тут не при чем

IO is a monad, but not the Monad

"IO -- монада", но не "IO -- это монада"

Вот так наверное

есть "монада IO", которая не тип, одноименная конструктору типов IO, который не монада сам по себе, но часть монады вместе с парой функций

когда говорят "f тут монада" это сокращение для более корректной формулировки, это не утверждение, что f ЯВЛЯЕТСЯ монадой

есть языки (с баундед полиморфизмом) где обсуждаемая интуиция правильна, но хаскель не из этих языков

"IO -- монада", но не "IO -- это монада"

нет разницы

когда говорят "f тут монада" это сокращение для более корректной формулировки, это не утверждение, что f ЯВЛЯЕТСЯ монадой

я не могу принять вашу семантику слова "является"

давайте вместо "является" говорить "is-a" или "is-the". kak eto budet po-russki?

нет разницы

Есть иногда. Например "Петя — врач", всё нормально, но если скажешь "Петя — это врач", то это будет уже не по-русски, как будто даёшь определение Пети через врача.

Есть иногда. Например "Петя — врач", всё нормально, но если скажешь "Петя — это врач", то это будет уже не по-русски, как будто даёшь определение Пети через врача.

Выражение "А — это Б" больше похоже на определение А через Б, а не на свойство А являться Б.

да какая разница, как это будет по русски, как это в хаскеле будет вот в C# легко доказать, что T это C C foo<T>(T t) where T : C => (C)t теперь докажите, что в хаскеле t это C C t => t -> C t; foo = ???

давайте вместо "является" говорить "is-a" или "is-the". kak eto budet po-russki?

в хаскеле отношения is-a между классом и типом для которого он имлпементирован нет, нельзя их кастить

Выражение "А — это Б" больше похоже на определение А через Б, а не на свойство А являться Б.

да, действительно

возможно какой-нибудь Maybe будет более чётким примером для тезиса "монада — это конструктор типов и две операции"

для Maybe можно определить не одну монаду, а штук пять разных

да и даже просто список, на нём вроде тоже не одну монаду определить можно

да какая разница, как это будет по русски, как это в хаскеле будет вот в C# легко доказать, что T это C C foo<T>(T t) where T : C => (C)t теперь докажите, что в хаскеле t это C C t => t -> C t; foo = ???

Давайте говорить как Хаскельбуржцы!

в хаскеле отношения is-a между классом и типом для которого он имлпементирован нет, нельзя их кастить

опять вы какой-то кастинг выдумываете

в хаскеле отношения is-a между классом и типом для которого он имлпементирован нет, нельзя их кастить

тем более, можно, только не напрямую, а через обёртку

тем более, можно, только не напрямую, а через обёртку

нет, нельзя

нет, нельзя

Exist доказывает, что можно

нет, не доказывает

вот для сишарпа я доказал в одну строчку, вот и вы попробуйте докажите свои утверждения

тем временем решение о том, чтоб не ломать зиллион пакетов с дженериками в 8.6 проходит "рулевой" процесс, пока что на гитхабе.

да какая разница, как это будет по русски, как это в хаскеле будет вот в C# легко доказать, что T это C C foo<T>(T t) where T : C => (C)t теперь докажите, что в хаскеле t это C C t => t -> C t; foo = ???

Что в хаскель коде написано вообще? С это одновременно и тайпкласс, и конструктор типа?

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

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

Это потому что подтипов нет?

Ага, типы не налазят!

да какая разница, как это будет по русски, как это в хаскеле будет вот в C# легко доказать, что T это C C foo<T>(T t) where T : C => (C)t теперь докажите, что в хаскеле t это C C t => t -> C t; foo = ???

я плохо знаю сишарп. что здесь написано? в частности, как определено С? что именно это доказывает?

Объект, написавший больше 10К строк на хаскиле?

Но при этом не Template Haskell

я плохо знаю сишарп. что здесь написано? в частности, как определено С? что именно это доказывает?

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

Завтра в breaking news "Выяснилось, что IO — это не монада. Хаскелисты присматриваются к си-шарп"

да какая разница, как это будет по русски, как это в хаскеле будет вот в C# легко доказать, что T это C C foo<T>(T t) where T : C => (C)t теперь докажите, что в хаскеле t это C C t => t -> C t; foo = ???

foo :: c t => t -> Exists c foo = Exists с объектом Exists c можно делать то же, что со ссылкой на суперкласс/интерфейс

я плохо знаю сишарп. что здесь написано? в частности, как определено С? что именно это доказывает?

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

по-моему, тайпклассами можно покрыть и ограничение, накладываемое супертипом, и многое другое

foo :: c t => t -> Exists c foo = Exists с объектом Exists c можно делать то же, что со ссылкой на суперкласс/интерфейс

это не то

это не то

почему?

потому что C это не Exists C

потому что C это не Exists C

в чём разница?

для начала в кайндах

потому что C это не Exists C

можно сказать, что в сишарпе передача по ссылке на интерфейс, а не объекта интерфейса, так что с одной стороны будет Ref C можно переименовать Exists в Ref, тогда с другой стороны будет тоже Ref C

для начала в кайндах

чтобы говорить о кайндах, сначала покажите мне тайпклассы в Сишарпе и подтипы в Хаскеле

нельзя сравнивать кайнды между языками

я сравниваю кайнды Constraint и Type в одном языке

я сравниваю возможности, они примерно одинаковые

я сравниваю кайнды Constraint и Type в одном языке

Exists C :: Type

ссылка на интерфейс — тоже тип

если сравнивать возможности, то у хаскеля они намного больше, речь не про возможности, а про то является ли ограничение тем, что оно ограничивает

если философствовать, то роза является только розой

Exists C :: Type

правильно, а C :: Type -> Constraint

а если писать код, то можно работать с T, обращаясь к нему только по констрэйнту

правильно, а C :: Type -> Constraint

это ничему не противоречит

если философствовать, то роза является только розой

философствуете вы, я говорю о том, эквивалентность чего можно или нельзя доказать в языке

это ничему не противоречит

это значит что вы не сконструируете доказательство C :~: Exists C на чем разговор можно закончить

это значит что вы не сконструируете доказательство C :~: Exists C на чем разговор можно закончить

с чего вы взяли, что я хотел доказать это?

т.е. вы не утверждаете, что C это то Exists C?

я утверждаю, что для программиста между C и Exists C нет принципиальной разницы

можно сказать, что в сишарпе передача по ссылке на интерфейс, а не объекта интерфейса, так что с одной стороны будет Ref C можно переименовать Exists в Ref, тогда с другой стороны будет тоже Ref C

про ссылку вообще не понятно

наверное, можно даже написать изоморфизм

я утверждаю, что для программиста между C и Exists C нет принципиальной разницы

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

про ссылку вообще не понятно

какая часть непонятна?

да никакая, если честно

а что сказать про нульарные констрейты (ну в смысле без привызяки к типам вообще)?

что?

это значит что вы не сконструируете доказательство C :~: Exists C на чем разговор можно закончить

{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} module Exists where import Data.Type.Equality data Exists c where Exists :: c a => a -> Exists c class (To a ~ b, From b ~ a) => Iso (a :: ka) (b :: kb) where type To a :: kb type From b :: ka instance Iso c (Exists c) where type To c = Exists c type From (Exists c) = c

и дальше что?

и дальше что?

это вы хотели формального доказательства

а я всего лишь утверждал, что можно решать одинаковые задачи

каста что-то все не видно

суть в том, что каст не нужен в Хаскелле