Тензорное определение с произвольно вложенными Vects - PullRequest
Новая
       32

Тензорное определение с произвольно вложенными Vects

1 голос
/ 12 апреля 2020

Я пытаюсь создать тип Tensor, но у меня возникают проблемы при работе с сигнатурой типа для конструктора. В этом и этом вопросе они определяют Tensor как Vect из Tensor с, а в этом вопросе как псевдоним типа для вложенный Vect с, но ни один не подходит для моих целей. Мне нужно, чтобы Tensor был атомом c (он не сделан из других Tensor s), и отличным типом (он не наследовал методы в силу своего псевдонима).

I попробовал следующее, которое неявно извлекает форму и тип данных из произвольно вложенного Vect через array_type и оборачивает его в минимальный Tensor тип 

import Data.Vect

total array_type: (shape: Vect r Nat) -> (dtype: Type) -> Type
array_type [] dtype = dtype
array_type (d :: ds) dtype = Vect d (array_type ds dtype)

data Tensor : (shape: Vect r Nat) -> (dtype: Type) -> Type where
  MkTensor : array_type shape dtype -> Tensor shape dtype

, который я тогда определил различные функции, чтобы проверить, работает ли он вообще (не включены здесь). Все это прекрасно компилируется, но когда я пытаюсь определить функцию для умножения каждого элемента на два, я попадаю в настоящую путаницу. Я пытался сначала определить его для вложенного Vect: 

times_two : Num dtype => array_type shape dtype -> array_type shape dtype
times_two (x :: xs) = (times_two x) :: (times_two xs)
times_two x = 2 * x

, но я получаю

При проверке левой стороны times_two:
При проверке применение Main.times_two:
Невозможно устранить неоднозначность, поскольку ни одно имя не имеет подходящего типа:
Prelude.List. ::, Prelude.Stream. ::, Data.Vect. ::

Замена :: на Data.Vect.:: не помогла. Возможно ли то, что я пытаюсь сделать? а толковый?

1 Ответ

1 голос
/ 12 апреля 2020

Нельзя сопоставить с array_type shape dtype, поскольку это не тип данных. Вам нужно выяснить (т.е. сопоставить), что означает shape, прежде чем этот тип упростится до типа данных. 

times_two {shape = []} x = 2 * x
times_two {shape = n :: ns} xs = map times_two xs

(В этом случае совпадение на xs находится внутри map.)

...