Experiment with differentiation via typeclasses - #10
Conversation
| Map f (x ': xs) = f x ': Map f xs | ||
|
|
||
| -- | Creates a list of indices into a type-level list. | ||
| type Fins :: forall {k} (l :: [k]) . [k] -> [Fin l] |
There was a problem hiding this comment.
Кажется, тут лучше
type Fins :: forall {k}. forall (l :: [k]) -> [Fin l]если такое компилируется
There was a problem hiding this comment.
Или просто forall l -> [Fin l], как в сигнатуре для (!)
| type family Args (i :: [[Natural]]) e :: Type where | ||
| Args i e = Rec At (Fins @(ArgsL i e) (ArgsL i e)) | ||
|
|
||
| type family Fun (i :: [[Natural]]) (o :: [Natural]) e :: Type where |
There was a problem hiding this comment.
можно просто type Fun i o e = ... вместо тайпфэмили
|
|
||
| data (:.:) f1 f2 = f1 :.: f2 | ||
|
|
||
| instance (Functional f1 i1 o1 e, Functional f2 (o1 : i2) o2 e, i ~ i1 ++ i2) => Functional (f1 :.: f2) i o2 e where |
There was a problem hiding this comment.
Почему не просто
(Functional f i j e, Functional g j k e) => Functional (f :.: g) i k eThere was a problem hiding this comment.
В текущей постановке тебе нужно как-то прокинуть в этот инстанс свидетель разделения i ~ i1 ++ i2, по которому в рантайме рекорд можно будет разбить на две части
There was a problem hiding this comment.
Потому что кайнды не сходятся. В конце концов, хочется иметь отображение из многих тензоров в один (таковым является, например, матмул), а тут j одновременно и как параметр, и как результат.
There was a problem hiding this comment.
Тогда, видимо, в качестве первого шага в композиции нужно класть список "функций", а не одну функцию. Либо сорить вспомогательной штукой которая переставляет входные аргументы
There was a problem hiding this comment.
Либо делать так, чтобы "функция" могла возвращать много тензоров, а не один, но это без гетерогенных индексов не выражается
| ArgsL '[] e = '[] | ||
| ArgsL (x ': xs) e = NDArr x e : ArgsL xs e | ||
|
|
||
| type family Args (i :: [[Natural]]) e :: Type where |
There was a problem hiding this comment.
Тут бтв тоже просто type вместо type family можно
2 participants
No description provided.