расширение TypeFamilies для этого нужно

это и есть те семейства

🤔 а как это относится к семействам

class Foo a where data X a :: * ...

ну тут X - тайп-левел функция (семейство типов), отдающая тип для некого a

@qnikst у тебя стек прекратил про shadowed dependencies говорить?

не знаю, я не тестил

у меня сегодня минимум 10 раз случилось

у тебя stack из гита?

я начинаю потихоньку принимать сторону тони морриса

а там из гита надо?

да

они так и не релизнули пофикшенное

там какой-то флаг обновления стека есть

чтобы из гита брал

аааа

о, спасибо

я уж пуллить полез

ну тут X - тайп-левел функция (семейство типов), отдающая тип для некого a

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

type X String = X в инстансе

он мне на класс ругается: class MyClass a where type MyAssociatedType :: *

P.S. Я догадываюсь что я занимаюсь ерундой и мне надо просто двинуть мой дататайп к классам, но тем не менее интересно можно ли такую проблему в принципе решить

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

а когда там будут нормальные сообщения с ошибками в ghc?

т.к. таким образом оно решается

в 8.2 что не устраивает?

а когда там будут нормальные сообщения с ошибками в ghc?

это какие?

разве что —explain нету

а уже добавили?

The associated type ‘MyAssociatedType’ mentions none of the type or kind variables of the class MyClass m’

class C a where type X a :: * f :: X a -> a data X' = X' String instance C String where type X String = X' f (X' s) = s

те как в расте

@saksmt ты очень невнимательно переписал, то что я написал

type X a

сообщение об ошибке это терминусом по консоли написало

те как в расте

а в расте какие?

как в 8.2 выделяется и ещё номер ошибки

по номеру можно сделать rustc —explain

ну там подчеркивает места где ошибка, а не просто выдает line:column

т.е. как в кланге?

и оно man page покаэет

т.е. как в кланге?

а да

@anarchostatist это уже в 8.2 есть

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

нет

спасибо!

у идриса же похожий синтаксис

ну разве что запостить на stack-overflow

и подождать пока перепишут

норм способ

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

/me ушёл смотреть анимешки

как я понимаю, coq сейчас самый активноюзаемый прувер в продакшене. И у него есть фича генерить код на хаскеле. Насколько это используют вообще?

тут все веобу чтоли

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

прувер в продакшене лол

смешно

но хз можно ли им доверять

ну вон в касперском хотели что-то прувать, не херней же они там маются

тут все веобу чтоли

как что-то плохое

я тоже кой-чего прувил, но фраза от этого не менее смешная

type X a

а для type X такое сделать нельзя? data у меня не параметризована в коде (просто не удачный пример привёл), равно как и то где она используется: data X class C m where a :: X -> m () —- data X = X String instance C SomeMonad where a x = {- implementation using x -}

вот же я код скинул

class C a where type X a :: * f :: X a -> a data X' = X' String instance C String where type X String = X' f (X' s) = s

Тут же оно от a зависит, который надо добавлять в параметры класса

X внутри класса - это не просто тип, это функция, которая вернет тип для типа, для которого делают инстанс, поэтому у нее должен быть аргумент

аааа

тут a не имеет ничего общего с a в классе?

имеет, это и есть тот a

но у тебя a и так есть в классе

Можно в хаскеле объявить абстрактный тип и его реализацию в другом модуле? что-то типа такого: module A where data X class MyClass a where a :: X -> a —- module B where import A data X = X String instance MyClass String where a (X v) = v

ты же для этого a потом инстанс делаешь

мой код выше - это полностью завершенный код, который тебе нужен, только имена переменуй. Никаких лишних переменных я не добавлял

вот так понятнее, думаю {-# LANGUAGE TypeFamilies, TypeSynonymInstances, FlexibleInstances #-} class C a where type GetTypeFor a :: * f :: GetTypeFor a -> a data X = X String instance C String where type GetTypeFor String = X f (X s) = s

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

чувак

посмотри на код

я тут мимо крокодил, но вы что-то странное делаете

X имеет каинд *

смысл упражнения “объявить абстрактный тип и его реализацию в другом модуле” в чем?

в другом пакете я бы понял