а если закрытое семейство?

а вот так если делать, то ошибки нет, она внутри сидит


*Main> :kind! Test2
Test2 :: Sigma [Nat] (Elem 1)
= MkSigma '[2, 3, 4] ('There ('There ('There (TypeError ...))))

если эту проблему решить, то общий Auto в целом получается

а ну хотя этот Auto вообще всегда будет подходить

Я тут чего-то наворотил странного чтобы эту TypeError вытащить наверх:

type Test = ListWith1' @[0,1,2,3] ElemAuto -- ok
type Test2 = ListWith1' @[0,4,2,3] ElemAuto -- error

type ListWith1' :: forall xs. Elem 1 xs -> ListWith1T xs
type family ListWith1' x where
  ListWith1' Nowhere = TypeError (Text "test")
  ListWith1' @xs x = ListWith1 @xs x

type ElemAuto :: forall x xs. Elem x xs
type family ElemAuto where
  ElemAuto @x @xs = App (Count 1 x xs)

type family Count acc x xs :: Nat where
  Count acc x (x:xs) = acc
  Count acc x (y:xs) = Count (acc + 1) x xs
  Count acc x '[] = 0

type App :: Nat -> Elem x xs
type family App n where
  App 0 = Nowhere
  App 1 = Here
  App n = There (App (n-1))

Но это не сильно помогло:

:kind! Test2
Test2 :: ListWith1T '[0, 4, 2, 3]
= (TypeError ...)

да полагаю дело не в вытаскиваннии

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

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

У терма он по техническим причинам возникнуть не может

Так что да

Привет всем)) На работе по необходимости нужно научиться кодить на хаскеле)
С чего бы лучше начать?

Если важно , за плечами С++ со всеми вытекающими

МОЖНО

начать с этого чата: @haskell_learn :) там есть подборка материалов для начинающих

В целом это офигенно! Много бойлерплейта если что-то ещё добавлять к этому Auto, но офигенно!

Интересно, а что это за работа такая? Не Касперский случаем?

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

Интересно еще для чего просят изучить, для общего развития (странно но why not), или собираются перекатываться на хаскелль

собираются переписать что-то с хаскеля на плюсы

Коммон практис?

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