Телеграмм чат группы haskellru страница 12982

Jerzy Syrowiecki

а также IsString

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

14:54пожаловаться #1

a

Имеется простая тайп фемили

type family Conc (a :: [*]) (b :: [*]) = (r :: [*]) | r -> a b
type instance Conc a '[] = a
type instance Conc a (x ': xs) = x ': Conc a xs

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

RHS of injective type family equation is a bare type variable
  Conc a '[] = a

Что не удивительно, так как у нас нет никаких гарантий что тайпфемили тотальны, однако задача как раз и заключается в то, что нужно как-то построить Conc с пруфом что r зависит от a и b, это вообще возможно?

15:12пожаловаться #2

DR

Denis Redozubov in Haskell

инъективные ТФ в текущей реализации не могут несколько параметров после | иметь, насколько я помню

15:15пожаловаться #3

JS

Имеется простая тайп фемили

type family Conc (a :: [*]) (b :: [*]) = (r :: [*]) | r -> a b
type instance Conc a '[] = a
type instance Conc a (x ': xs) = x ': Conc a xs

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

RHS of injective type family equation is a bare type variable
  Conc a '[] = a

Что не удивительно, так как у нас нет никаких гарантий что тайпфемили тотальны, однако задача как раз и заключается в то, что нужно как-то построить Conc с пруфом что r зависит от a и b, это вообще возможно?

в этой формуле из r не выводится a b

15:18пожаловаться #4

JS

а зачем здесь эта зависимость?

15:21пожаловаться #5

a

Jerzy Syrowiecki

а зачем здесь эта зависимость?

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

15:22пожаловаться #6

к

Имеется простая тайп фемили

type family Conc (a :: [*]) (b :: [*]) = (r :: [*]) | r -> a b
type instance Conc a '[] = a
type instance Conc a (x ': xs) = x ': Conc a xs

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

RHS of injective type family equation is a bare type variable
  Conc a '[] = a

Что не удивительно, так как у нас нет никаких гарантий что тайпфемили тотальны, однако задача как раз и заключается в то, что нужно как-то построить Conc с пруфом что r зависит от a и b, это вообще возможно?

не понимаю,

вот имею результат '[1, 2, 3]

какие соответствия a и b?

15:22пожаловаться #7

к

я по твому определению вижу аж 2 варианта

15:22пожаловаться #8

к

у тебя неверная зависимость, я к этому веду

15:23пожаловаться #9

a

я понял, да

15:23пожаловаться #10

a

однако

15:23пожаловаться #11

JS

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

но это невозможно

пусть справа x : Conc a xs, тогда слева либо Conc (x : Conc a xs) [], либо Conc a (x : xs), нет однозначности

15:25пожаловаться #12

к

вроде бы все зависимости для такого тела:
a b -> r (бессмысленная зависимость, так как семейства это функции, а все функции по определению обладают такой зависимостью)
a r -> b
b r -> a

15:25пожаловаться #13

к

Имеется простая тайп фемили

type family Conc (a :: [*]) (b :: [*]) = (r :: [*]) | r -> a b
type instance Conc a '[] = a
type instance Conc a (x ': xs) = x ': Conc a xs

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

RHS of injective type family equation is a bare type variable
  Conc a '[] = a

Что не удивительно, так как у нас нет никаких гарантий что тайпфемили тотальны, однако задача как раз и заключается в то, что нужно как-то построить Conc с пруфом что r зависит от a и b, это вообще возможно?

> с пруфом что r зависит от a и b, это вообще возможно?
а кек, это по дефолту уже

зависимость простая, для любых a и b, r = Conc a b

15:28пожаловаться #14

DR

Denis Redozubov in Haskell

Jerzy Syrowiecki

в этой формуле из r не выводится a b

тут конкретно - нет, но это в целом в GHC недореализовано

15:28пожаловаться #15

JS

кана

> с пруфом что r зависит от a и b, это вообще возможно?
а кек, это по дефолту уже

зависимость простая, для любых a и b, r = Conc a b

вероятно, автор хотел сказать наоборот

15:28пожаловаться #16

JS

кана

вроде бы все зависимости для такого тела:
a b -> r (бессмысленная зависимость, так как семейства это функции, а все функции по определению обладают такой зависимостью)
a r -> b
b r -> a

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

15:29пожаловаться #17

к

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

Зигохистоморфный Пре... in Haskell

15:30пожаловаться #18

ЗП

я уже вроде задавал вопрос, но ответа не получал)
так вот как можно заменить это на что-то типа coerce?

https://gist.github.com/xgrommx/e828cb7c9e96f4283b41e6c154d87149#file-alg2-hs-L13-L22

Gist

Alg2

Alg2. GitHub Gist: instantly share code, notes, and snippets.

Александр Гранин... in Haskell

15:34пожаловаться #19

АГ

А кто-нибудь читал A type of programming? Меня озадачивает, что автор пишет и пишет, и я не понимаю по отрывкам, о чем эта книга