Haskell: как параметризовать тип целым числом?

[warlock66613]

Допустим, есть библиотека матриц произвольной размерности (https://hackage.haskell.org/package/matrix-0.3.5.0/docs/Data-Matrix.html#g:3).
И я хочу дефинировать, что матрицы одинаковой размерности образуют группу по сложению (http://hackage.haskell.org/package/vector-space-0.10.4/docs/Data-AdditiveGroup.html#t:AdditiveGroup).

Попробуем:

Используется синтаксис Haskell

instance AdditiveGroup a => AdditiveGroup (Matrix a) where
  zeroV = ???

Мы должны создать нулевую матрицу, но мы не знаем какой размерности!

Конечно, можно создать специальные типы MD1x1, MD1x2, MD2x1, MD2x2, ... и использовать их как параметры, и тогда всё получится, но я не верю, что, учитывая мощные возможности GHC (такие как TemplateHaskell и т. п.), нельзя сделать более красиво.

Есть идеи?

[Xaositect]

В современных версиях GHC есть такие возможности (расширение DataKinds, модули GHC.TypeLits, Data.Proxy).

Вот пример использования, похожий на то, что Вам надо: https://github.com/fhaust/aer-utils/blo ... mpleMat.hs

[warlock66613]

Xaositect, спасибо, это действительно то, что надо.

[warlock66613]

Почему-то не получается:

Используется синтаксис Haskell

newtype Mat (r :: Nat) (c :: Nat) a = Mat (Matrix a)

mrows :: forall r c a . KnownNat r => Mat r c a -> Int
mrows _ = fromInteger $ natVal (Proxy :: Proxy r)
 

Ответ компилятора:

1. • Couldn't match kind ‘*’ with ‘Nat’ 
2.   When matching the kind of ‘Proxy’ 
3. • In the first argument of ‘natVal’, namely ‘(Proxy :: Proxy r)’ 
4.   In the second argument of ‘($)’, namely ‘natVal (Proxy :: Proxy r)’ 
5.   In the expression: fromInteger $ natVal (Proxy :: Proxy r) 

[Xaositect]

GHC не знает, что r в теле функции - это то же самое r, что и в объявлении типа. Нужно расширение ScopedTypeVariables.

Используется синтаксис Haskell

{-# LANGUAGE DataKinds, KindSignatures, ScopedTypeVariables, Rank2Types #-}

module Temp where

import GHC.TypeLits
import Data.Proxy

type Matrix a = [[a]]

newtype Mat (r :: Nat) (c :: Nat) a = Mat (Matrix a)

mrows :: forall r c a. KnownNat r => Mat r c a -> Int
mrows _ = fromInteger $ natVal (Proxy :: Proxy r)
 

[warlock66613]

Xaositect, да, точно. Спасибо ещё раз, вроде получилось (во всяком случае скомпилировалось.

(Мне очень нравится Haskell, но этот ЯП не просто умнее меня, а просто страшно представить насколько умнее.)

[_Ivana]

На правах дилетанта позволите уточнить пару вопросов?

1) Вы предусматриваете каким-либо образом на этапе компиляции контроль одинаковых размерностей матриц при операциях с ними? Без создания своих типов для каждой размерности.

2) Если нет, то почему бы не выбрать в качестве нейтрального элемента просто бесконечный по всем измерениям тип, который участвует в операциях с элементами того же типа любых размерностей? С двумерными матрицами сложнее, возьмем одномерные вектора нефиксированной длины. Группу по сложению не стал рисовать, но на примере моноида идея видна:

Используется синтаксис Haskell

import Data.Monoid

newtype Vec a = Vec [a] deriving Show

instance Monoid a => Monoid (Vec a) where
    mempty = Vec $ repeat mempty  
    Vec a `mappend` Vec b = Vec $ zipWith mappend a b

main = print $ Vec (map Sum [1..3]) <> Vec (map Sum [10..])

[arseniiv]

_Ivana в сообщении #1194230 писал(а):

1) Вы предусматриваете каким-либо образом на этапе компиляции контроль одинаковых размерностей матриц при операциях с ними? Без создания своих типов для каждой размерности.

Да, тут это вроде как раз и происходит. Один тип с киндом Nat -> Nat -> * -> *, после применения типов-размерностей и типа значений элементов матриц остаётся *, тип со значениями.

[_Ivana]

arseniiv спасибо, понятно. Тогда отзываю предложенную халтуру