@haskellru

Страница 407 из 1551
 
Vyacheslav
16.09.2017
12:58:10
как это лучше через тип выразить?

 
Alexander
16.09.2017
12:58:31
через гадты и дата кайндс

 
Index
16.09.2017
12:58:54
"Поле A зависит от поля B" порождает два варианта: 1. симулировать зависимые типы через синглтоны (не советую, это хардкор) 2. сделать sum-тип и написать коммент про инвариант (классный и тупой Haskell98)

 
Vyacheslav
16.09.2017
12:59:14
через гадты и дата кайндс
вот этот вариант нравится, сам о нем думал

Google
 
Alexander
16.09.2017
12:59:19
ну сигнлтоны не факт что нужны

 
но если будешь далеко заходить, то до них дойдет

 
Index
16.09.2017
12:59:37
Твое предложение (gadt-ы и datakinds) равносильно синглтонами

 
Vyacheslav
16.09.2017
12:59:41
но пока не понимаю как это стоит сделать

 
Index
16.09.2017
12:59:46
даже есть data family Sing не использовать, принцип там примерно тот же будет

 
Alexander
16.09.2017
12:59:54
принцип тот же

 
Vyacheslav
16.09.2017
13:00:09
а можно пример где-то?

 
глянуть того о чем вы говорите

 
Alexander
16.09.2017
13:00:22
но написать проще свое,чем использовать большую и страшную либу

 
мне с телефона не удобно, вечером могу, часов после 9 мск

 
Index
16.09.2017
13:01:56
а можно пример где-то?
на примере твоей задачи. Ты хочешь написать тип вроде data Response = Response (p :: Parameters) (Action p), где Action это type family, которая зависит от p (параметров)

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

 
Vyacheslav
16.09.2017
13:02:35
да про это я в курсе

Google
 
Index
16.09.2017
13:02:40
Соответственно извращаться надо в направлении того, чтобы был параметр p на типах, а не на тёрмах

 
Vyacheslav
16.09.2017
13:02:44
в idris я бы эту проблему давно решил(

 
Index
16.09.2017
13:02:55
А, ок. Тогда просто бери синглтоны

 
Там идея в том, чтобы отразить тёрм на типах

 
data Bool = False | True data SBool (b :: Bool) where STrue :: SBool 'True SFalse :: SBool 'False

 
соответствие 1-к-1

 
Если у тебя известен b в SBool b, то ты знаешь, какой у тебя тёрм (можешь синтезировать)

 
Если у тебя есть тёрм с некоторыми типом SBool b, то паттерн-матчингом узнаешь параметр b.

 
В итоге ходишь туда-сюда между этими представлениями Bool, в зависимости от того, надо тебе ссылаться на значение в типах, или не надо.

 
если экзистенциально квантифицировать, то exists b. SBool b полностью эквивалентно Bool

 
Это можно даже в коде отразить data SomeBool = forall b. SomeBool (SBool b) f :: SomeBool -> Bool g :: Bool -> SomeBool f . g = id g . f = id

 
Делаешь аналогичное для Parameters

 
Чтобы поменьше писать вручную, есть страшненькая, но сравнительно удобная библиотека singletons.

 
illiatshurotshka❄️
16.09.2017
13:08:39
здесь нужен forall?

 
Vyacheslav
16.09.2017
13:08:49
примерно понял, буду разбираться

 
спасибо

 
Alexander
16.09.2017
13:13:26
на примере твоей задачи. Ты хочешь написать тип вроде data Response = Response (p :: Parameters) (Action p), где Action это type family, которая зависит от p (параметров)
я подозреваю что можно проще если Action не общая функция

 
Index
16.09.2017
13:14:51
Да, можно выделить набор возможных вариантов для Action, типа actionType, и иметь Parameters actionType и Action actionType

 
illiatshurotshka❄️
16.09.2017
14:26:20
возможно ли написать функцию map для data Meme = forall a. Meme [a] ?

 
kana
16.09.2017
14:29:07
Ну это будет не функтор как минимум, потому что Meme : *, а не * -> *

Google
 
illiatshurotshka❄️
16.09.2017
14:29:56
если я правильно понимаю то такая функция принимала бы только id

 
kana
16.09.2017
14:31:08
(forall a. a) -> (forall a. a) Хз даже

 
Vasiliy
16.09.2017
14:41:03
почему же только id, const 42 тоже вполне подходит

 
Index
16.09.2017
15:08:22
Не подходит

 
kana
16.09.2017
15:10:07
Даже id же не подходит

 
illiatshurotshka❄️
16.09.2017
15:10:12
оо

 
почему?

 
kana
16.09.2017
15:11:22
Ну так id возвращает то же, что и принимает, то есть конкретный тип. А нужно вернуть (forall a. a)

 
Сработает, если вернуть undefined

 
const undefined

 
Теоретически

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

 
Index
16.09.2017
15:16:38
id подошел бы с impredicative types

 
Иначе придется писать \x -> x

 
То есть тёрм подходит, но типы не унифицируются.

 
А тип мапы будет (forall a. a -> a) -> Meme -> Meme

 
Поэтому только id из тотальных функций

 
const undefined тоже подойдет

 
Может еще seq какой-нибудь.

 
kana
16.09.2017
15:22:35
Хм, значит я все примерно правильно понимаю

Google
 
illiatshurotshka❄️
16.09.2017
15:27:07
а что вообще значит f в (forall x. x -> f x) -> (a, b) -> (f a, f b)?

 
kana
16.09.2017
15:28:58
Любой f : * -> * же

 
Index
16.09.2017
15:28:58
Некий функтор, видимо

 
Ну то есть любой ☆ -> ☆, но буква обычно f для таких штук из-за того, что чаще всего это функторы

 
kana
16.09.2017
15:30:45
Звёздочку нашел, а стрелочку нет)

 
Index
16.09.2017
15:30:59
Такая клавиатура на телефоне

 
kana
16.09.2017
15:31:12
Оп, че за клава?

 
Index
16.09.2017
15:31:12
Стрелочки нет ?

 
Samsung Note дефолтная

 
illiatshurotshka❄️
16.09.2017
15:31:32
а (forall x. forall y. x -> y -> f x y) это любой * -> * -> * ?

 
Index
16.09.2017
15:32:21
Да и звездочка контурная у меня, а не правильная

 
°•○●□■♤♡◇♧☆▪¤《》¡¿

 
Вот такой тут репертуар, Агду не попишешь

 
а (forall x. forall y. x -> y -> f x y) это любой * -> * -> * ?
Да

 
illiatshurotshka❄️
16.09.2017
15:33:02
оок спс

 
Abbath
16.09.2017
16:58:27
https://github.com/neovimhaskell/nvim-hs

 
Vyacheslav
16.09.2017
17:48:41
я все еще туплю с тем как заимплементить то что мне нужно

 
я хочу сделать что-то вроде вот такого

 
singletons [d| data AIIntent = IntentTask |] data AIResult a where AIResult :: SAIIntent b -> (actionToParam b) -> AIResult b

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

Google
 
Vyacheslav
16.09.2017
17:53:19
я сейчас просто не понимаю, как написать этот actionToParam

 
блин, наткнулся на это и все понял

 
https://ocharles.org.uk/blog/posts/2014-02-25-dependent-types-and-plhaskell.html

 
illiatshurotshka❄️
16.09.2017
18:10:55
× в сигнатуре типа значит cartesian product? (например (∃c. c × (A × c → B)) × A → B )

 
Arseniy
16.09.2017
18:11:28
Олли офигенный чувак

 
kana
16.09.2017
18:13:12
ну да, пара просто

 
+ же - Either

 
b^a - a -> b

 
illiatshurotshka❄️
16.09.2017
18:14:11
пара либо любой тип эквивалентный паре?

 
kana
16.09.2017
18:14:40
любой изоморфный

 
Pair a b = Pair a b Pair меняем на (,) (,) a b = (,) a b

 
это первый пост в моем канале

 
illiatshurotshka❄️
16.09.2017
18:15:42
то есть Either (a, b) Void, к примеру, не считается?

 
kana
16.09.2017
18:16:42
Either (a, b) Void это то же самое, что и (a, b)

 
a*b + 0 = a*b

 
illiatshurotshka❄️
16.09.2017
18:18:09
есть где почитать про использование алгебры для типов?

 
Abbath
16.09.2017
18:18:22
В TAPL?

 
kana
16.09.2017
18:19:37
https://codewords.recurse.com/issues/three/algebra-and-calculus-of-algebraic-data-types http://chris-taylor.github.io/blog/2013/02/10/the-algebra-of-algebraic-data-types/ http://chris-taylor.github.io/blog/2013/02/11/the-algebra-of-algebraic-data-types-part-ii/ http://chris-taylor.github.io/blog/2013/02/13/the-algebra-of-algebraic-data-types-part-iii/
вот

 
illiatshurotshka❄️
16.09.2017
18:24:04
крууто, а как ⊤ выражается?

 
kana
16.09.2017
18:26:24
мб какой тип-универсум, типа Type в идрисе

Страница 407 из 1551