class Contextual (container :: * -> [*] -> *)
class (∀a b (t :: a -> b -> *). Contextual t, Contains Fresh b ~ True) 
   => Canonnical t

В общем я подумал немного и по-моему так совсем нельзя. Что b не определено это понятно, если записать ∀a b (t :: a -> b -> *). Contains Fresh b ~ True => Contextual t то b в скоупе. А то там же кортеж, а forall связывается с элементом кортежа. Но всё равно не получится, потому что b не kind, и DataKinds не промоутятся. Поэтому сослаться на b :: [*] в kind-сигнатуре уже нельзя.

Более того, если b :: [*], то значит b ~ '[x, y, z, ...]. Но это довольно абсурдный kind даже если бы он промоутился! b :: [*] не значит что b ~ [*].

Я так понимаю идея в том чтобы привязаться к конкретному typelevel списку. Так это сделать не получится, у container никакого списка ещё нет, он его только ждёт. И ведь любой подойдёт ему.

Любой, который содержит тип фрэш.

По kind-сигнатуре вообще любой. Ограничить kind-сигнатурой типы в списке нельзя, это уже какие-то dependent kinds получаются

Чтож, ждём в ghc 10

я хотел както так

data Fresh
data HasLoad

class Contextual (container :: * -> [*] -> *) where
  init :: container () '[Fresh]

class (∀a b (t :: a -> b -> *). Contextual t, Contains Fresh b ~ True)
  => Canonnical t where
  write :: v -> t l b -> t v (HasLoad : Remove Fresh b)

депендент кайндс же где-то с 6.6 по 8.0 появились, смотря как считать

и куда они делись?

никуда не делись!

OwO

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

Поясните глубину мысли. Я провёл аналогию с завтипами, что тип зависит от терма. Тут человек хочет чтобы кайнд зависел от типа. Насколько я знаю систему kind-ов -- это не работает. Вы с TypeInType не путаете?

почему не работает-то?

Да вот я выше написал.

ниче не понятно

Ну стало быть Вы что-то сугубо своё имеете ввиду под dependent kinds :)

на типах полноценные завтипы есть, все будет работать

прям с пи, сигмой, завматчингом

наоборот я имею в виду общее, а выше написано че-то свое

"полноценных" ещё нет всё-таки. можно правда нахакать. но очень много бойлерплейта.

Обнаружилось, что на тайплевел хаскеле есть полноценные зависимые типы, в намного большем смысле чем просто "можно писать a -> (x :: a) -> ..."

Продолжаю изучать в поисках ограничений

Примеры:

- натуральные числа и несколько простых доказательств о коммутативности сложения и умножения:
https://gist.github.com/kana-sama/9185b30b45bd9817f11361e424a8abc7

- простое доказательство (x / 2) * 2 = x для всех четный натуральных чисел:
https://gist.github.com/kana-sama/b029dfa1b1665b207259b58588659a1a

- сигма-типы и работа с ними (тот же безопасный Half :: Even -> Nat)
https://gist.github.com/kana-sama/bd3ec6ddc19846665d9d1f632483550a

для сборки нужен ghc 8.10+

Из проблем:
- отсутствие лямбд приводит к тому, что все функции вида f (\x -> y) превращаются в специализированные топлевел функции, который делают то же самое

да где нет, если есть