вообще OVERLAPPABLE + {-# OVERLAPPING #-}

с некоторой долей олегинга можно наверное сказать

доп параметр дать + фундеп

@vlastachu ^

Здравствуйте

Пытаюсь разобраться с сервантом

Подскажите пожалуйста

Что означают вот эти две строки

api :: Proxy Api api = Proxy

тайп левел магию)

api :: Proxy Api api = Proxy

data Proxy (a :: k) = Proxy тут Proxy-тип - конструктор типа с фантомным аргументом-типом любого каинда по сути своей api - просто Proxy-значение с типом-фантомом Api нужен для того, чтобы на термлевеле контролировать передачу чего-то на тайплевел (в данном случае Api) idP :: Proxy a -> a -> a idP Proxy x = x x :: _ -- will be Int x = idP (Proxy :: Proxy Int) 1 stringProxy :: Proxy String stringProxy = Proxy y :: _ -- String y = idP stringProxy "123" z = idP stringProxy 1 -- type error, String /= Int (or no Num String)

простой пример использования (на самом деле можно заменить на TypeApplications)

А это случайно не Geometric Numerical Integration?

А что такое каинд?

А что такое каинд?

тип типа, а вооще есть чатик для начинающих

Вроде же писали что сюда можно задавать подобные вопросы

А это случайно не Geometric Numerical Integration?

оно

забавно через столько лет встретить снова в хаскель чате )

Вроде же писали что сюда можно задавать подобные вопросы

можно, сейчас отвечу

тип типа, а вооще есть чатик для начинающих

НЕТУ ЧАТИКА ДЛЯ НАЧИНАЮЩИХ!!!!1 азаза

ЕСТЬ @haskell_learn

забавно через столько лет встретить снова в хаскель чате )

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

ЕСТЬ @haskell_learn

хватит пиарить вредные вещи

что за кибербуллинг чатов

вообще смешно как-то работает

тут всех гонят в один

@al_bl https://wiki.haskell.org/Kind

а там всех гонят в другой

мол, эта тема не для начинающих

@al_bl если после прочтения будут вопросы, то можно попытаться по русски объяснить:)

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

уже один gitter так поломали

сепаратисты

А что такое каинд?

вот есть у нас терм 2, он имеет тип Int эта же логика переносится на уровень выше: есть у нас тип Int, он имеет каинд Type есть у нас терм-функция succ, которая принимает терм типа Int и отдает терм типа Int, то есть succ :: Int -> Int succ 2 :: Int эта же логика переносится на уровень выше: если конструкттор типа Maybe, который принимает тип каинда Type и отдает тип каинда Type, то есть Maybe :: Type -> Type Maybe Int :: Type есть функция $, которая принимает функцию типа (a -> b) и значение типа a, отдает значение типа b ($) :: (a -> b) -> a -> b f $ x = f x succ $ 2 == 3 есть тип $, который принимает конструктор типов (Type -> Type) и тип Type и отдает тип Type ($) :: (Type -> Type) -> Type -> Type type f $ x = f x Maybe $ Int == Maybe Int 1 :: Int :: Type не все типы имеют каинд Type или (Type -> k), где k - один из этих двух

уже один gitter так поломали

гиттер поломало существование телеграма (и несуществование [точнее, жалкое существование] мобильного гиттера). а с сепарацией всё ок

нет конечно

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

даже до появления этого

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

Спасибо большое

С каиндами понятно

class X a where f :: a -> Int newtype Z = Z Int instance X Z where f (Z x) = x instance X a => X (a, b) where f (x, _) = f x instance X b => X (a, b) where f (_, y) = f y x = f (0, (0, (Z 1, (0, 0)))) -- ожидаю 1 Duplicate instance declarations: instance X a => X (a, b) instance X b => X (a, b) вот тот пример, overlaps мне не помог никак почему не работает - понимаю, как решить задачу - нет

ну в конекст же не смотрит компилятор

X (a,b) == X (a,b)

можно через ~

в контексте

вот текущее рабочее рашение, но тут дублирование кода шаблона Z newtype Z = Z Int class X a where f :: a -> Int instance X Z where f (Z x) = x instance X (Z, b) where f (a, _) = f a instance {-# OVERLAPS #-} X b => X (a, b) where f (_, y) = f y x = f (0, (0, (Z 1, (0, 0))))

эм..

нужно же {-# OVERLAPABLE #-} X b и {-# OVERLAPS #-} X (Z,b)

Я понял что такое прокси

Но я не понимаю

Зачем его использовать

Час ушел

например у тебя есть код вида show . read

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

без type applciations

а ViewPatterns и lambda case можно как-то совместить в одно?

а ViewPatterns и lambda case можно как-то совместить в одно?

конечно)

а ViewPatterns и lambda case можно как-то совместить в одно?

https://twitter.com/xgrommx/status/833793370547961856

Спасибо, я уже не помню что я писал что оно у меня не работало :)

@kana_sama equality я ещё вижу как вытащить, но не произвольный констрейнт

получилось!

{-# LANGUAGE KindSignatures #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} import Data.Proxy class X a where f :: a -> Int newtype Z = Z Int instance X Z where f (Z x) = x data T = L | R type family IF t a b :: k where IF 'True a b = a IF 'False a b = b type family When t a :: k where When 'True a = a type family Or a b where Or 'True a = 'True Or a 'True = 'True type family XQ a where XQ Z = True XQ (a,b) = Or (XQ a) (XQ b) XQ c = False type family XQW z :: T where XQW (a, b) = IF (XQ a) 'L (When (XQ b) 'R) instance (z ~ (a,b), XX (XQW z) a b) => X (a,b) where f (a,b) = ff (Proxy @ (XQW (a, b))) a b class XX (t :: T) a b where ff :: proxy t -> a -> b -> Int instance X a => XX 'L a b where ff _ a _ = f a instance X b => XX 'R a b where ff _ _ b = f b x = f (0::Int, (0::Int, (Z 1, (0::Int, 0::Int))))

но это ужас хтонический

@kana_sama ^

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

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

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

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

как-то это через FD должно быть можно записать в т.ч. (наверное)

но чот я давно олеггирингом не занимался

но это ужас хтонический

Это да

Спасибо

а что, Nat из GHC.TypeLits нельзя матчить (чтобы S k забрать например)?

+ 1 использовать нельзя, он не *ективный

нельзя, он же не индуктивный

а к своим типам сахарок для литералов на тайплевеле нельзя прикрутить, верно?

чтобы они работали как литс вроде нет