даже есть data family Sing не использовать, принцип там примерно тот же будет

принцип тот же

а можно пример где-то?

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

но написать проще свое,чем использовать большую и страшную либу

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

а можно пример где-то?

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

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

да про это я в курсе

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

в idris я бы эту проблему давно решил(

А, ок. Тогда просто бери синглтоны

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

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.

здесь нужен forall?

примерно понял, буду разбираться

спасибо

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

я подозреваю что можно проще если Action не общая функция

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

возможно ли написать функцию map для data Meme = forall a. Meme [a] ?

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

если я правильно понимаю то такая функция принимала бы только id

(forall a. a) -> (forall a. a) Хз даже

почему же только id, const 42 тоже вполне подходит

Не подходит

Даже id же не подходит

оо

почему?

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

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

const undefined

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

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

id подошел бы с impredicative types

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

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

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

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

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

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

Хм, значит я все примерно правильно понимаю

а что вообще значит f в (forall x. x -> f x) -> (a, b) -> (f a, f b)?

Любой f : * -> * же

Некий функтор, видимо

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

Звёздочку нашел, а стрелочку нет)

Такая клавиатура на телефоне

Оп, че за клава?

Стрелочки нет 😔

Samsung Note дефолтная

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

Да и звездочка контурная у меня, а не правильная

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

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

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

Да

оок спс

https://github.com/neovimhaskell/nvim-hs

я все еще туплю с тем как заимплементить то что мне нужно

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

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

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

я сейчас просто не понимаю, как написать этот actionToParam

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

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

× в сигнатуре типа значит cartesian product? (например (∃c. c × (A × c → B)) × A → B )

Олли офигенный чувак

ну да, пара просто

+ же - Either

b^a - a -> b

пара либо любой тип эквивалентный паре?

любой изоморфный

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