Создание складки, которая позволяет типу изменять после каждого повторного вызова функции, чтобы вызвать функцию n раз без рекурсии

Я пытаюсь использовать dfold, определенный здесь

В основном это сводка, которая позволяет вам возвращать новый тип после каждого цикла.

Я две функции, важные для типов, которые dfold сгенерируют:

Пример, использованный в вышеупомянутом проекте:

С этой версией я могу быстро создавать новые битонические сортировки, например:

Каждый Сортировка с работой с вектором указанного размера.

Я хотел бы создать функцию, которая генерирует функцию для данного Vec. Я считаю, что использование dfold или dtfold - правильный путь здесь.

Я хотел сделать сложение с чем-то вроде функции genBitonic.

Затем используйте fst, чтобы получить нужную мне функцию для сортировки.

Один. Сложите композицию, чтобы получить функцию, которая берет базу.

До того, как база была ответила, это привело бы к чему-то вроде

Два: Вторая идея заключалась в том, чтобы использовать bitonicBase как значение b, чтобы начать накопление. Это привело бы непосредственно к форме, в которой я нуждаюсь, прежде чем применить fst.

Edit vecAcum предназначен только для создания значения внутри dfold.

В примере dfold они складываются с использованием :>, который является просто векторной формой оператора списка :

Что я хочу сделать, это взять кортеж из двух функций, таких как:

И составите их. Итак, genBitonic . genBitonic будет иметь тип:

Итак, базовая функция будет тем, что затвердевает типы. например.

Я использую dfold для построения функции для векторов длины n, которая эквивалентна выполнению рекурсии на векторе длины n.

Я попытался выполнить пример, указанный в dfold

Я использую расширения, которые использует исходный код dfold

** РЕДАКТИРОВАТЬ ** Добавлено гораздо больше деталей.

Ответы

Ответ 1

Ваш случай base был неправильным; это должно быть

base :: (Ord a) => SplitHalf a @@ 0
base = (id, bitonicMerge id)

Объединяя все вместе, здесь полная рабочая версия, протестированная на GHC 8.0.2 (но она должна работать все равно на CLASH на основе GHC 8.0.2 по модулю Prelude). Оказывается, вещь operationList не используется, кроме ее позвоночника, поэтому мы можем использовать вместо нее Vec n ().

{-# LANGUAGE DataKinds, GADTs, KindSignatures #-}
{-# LANGUAGE Rank2Types, ScopedTypeVariables  #-}
{-# LANGUAGE TypeFamilies, TypeOperators, UndecidableInstances #-}

{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise -fplugin GHC.TypeLits.KnownNat.Solver #-}
{-# OPTIONS_GHC -fno-warn-incomplete-patterns -fno-warn-redundant-constraints #-}

{-# LANGUAGE NoImplicitPrelude #-}
import Prelude (Integer, (+), Num, ($), undefined, id, fst, Int, otherwise)
import CLaSH.Sized.Vector
import CLaSH.Promoted.Nat
import Data.Singletons
import GHC.TypeLits
import Data.Ord

type ExpVec k a = Vec (2 ^ k) a

data SplitHalf (a :: *) (f :: TyFun Nat *) :: *
type instance Apply (SplitHalf a) k = (ExpVec k a -> ExpVec k a, ExpVec (k + 1) a -> ExpVec (k + 1) a)

generateBitonicSortN2 :: forall k a . (Ord a, KnownNat k) => SNat k -> ExpVec k a -> ExpVec k a
generateBitonicSortN2 k = fst $ dfold (Proxy :: Proxy (SplitHalf a)) step base (replicate k ())
  where
    step :: SNat l -> () -> SplitHalf a @@ l -> SplitHalf a @@ (l+1)
    step SNat _ (sort, merge) = (bitonicSort sort merge, bitonicMerge merge)

    base = (id, bitonicMerge id)

Это работает как ожидалось, например:

*Main> generateBitonicSortN2  (snatProxy Proxy)  testVec2
<9,2>
*Main> generateBitonicSortN2  (snatProxy Proxy)  testVec4
<9,8,6,2>
*Main> generateBitonicSortN2  (snatProxy Proxy)  testVec8
<9,8,7,6,3,2,1,0>
*Main> generateBitonicSortN2  (snatProxy Proxy)  testVec16
<9,8,8,7,7,6,6,5,4,3,3,2,2,1,0,0>
*Main>

Ответ 2

Я использую CLaSH для синтеза этого в VHDL, поэтому я не могу использовать рекурсию для применения t раз

Я не понимаю этого предложения, но кроме этого:

{-# LANGUAGE GADTs, DataKinds, TypeFamilies, UndecidableInstances,
      FlexibleInstances, FlexibleContexts, ConstraintKinds,
      UndecidableSuperClasses, TypeOperators #-}

import GHC.TypeLits
import GHC.Exts (Constraint)
import Data.Proxy

data Peano = Z | S Peano

data SPeano n where
  SZ :: SPeano Z
  SS :: SPeano n -> SPeano (S n)

type family PowerOfTwo p where
  PowerOfTwo  Z    = 1
  PowerOfTwo (S p) = 2 * PowerOfTwo p

type family KnownPowersOfTwo p :: Constraint where
  KnownPowersOfTwo  Z    = ()
  KnownPowersOfTwo (S p) = (KnownNat (PowerOfTwo p), KnownPowersOfTwo p)

data Vec (n :: Nat) a -- abstract

type OnVec n a = Vec n a -> Vec n a
type GenBitonic n a = (OnVec n a, OnVec (2 * n) a)

genBitonic :: (Ord a, KnownNat n) => GenBitonic n a -> GenBitonic (2 * n) a
genBitonic = undefined

bitonicBase :: Ord a => GenBitonic 1 a
bitonicBase = undefined

genBitonicN :: (Ord a, KnownPowersOfTwo p) => SPeano p -> GenBitonic (PowerOfTwo p) a
genBitonicN  SZ    = bitonicBase
genBitonicN (SS p) = genBitonic (genBitonicN p)

genBitonicN определяется рекурсией по числу peano, представляющему степень. На каждом рекурсивном шаге появляется новый KnownNat (PowerOfTwo p) (через семейство типов KnownPowersOfTwo). На уровне значения genBitonicN тривиально и просто делает то, что вы хотите. Однако для определения удобного bSortN:

нам нужны дополнительные механизмы,

type family Lit n where
  Lit 0 = Z
  Lit n = S (Lit (n - 1))

class IPeano n where
  speano :: SPeano n

instance IPeano Z where
  speano = SZ

instance IPeano n => IPeano (S n) where
  speano = SS speano

class (n ~ PowerOfTwo (PowerOf n), KnownPowersOfTwo (PowerOf n)) =>
         IsPowerOfTwo n where
  type PowerOf n :: Peano
  getPower :: SPeano (PowerOf n)

instance IsPowerOfTwo 1 where
  type PowerOf 1 = Lit 0
  getPower = speano

instance IsPowerOfTwo 2 where
  type PowerOf 2 = Lit 1
  getPower = speano

instance IsPowerOfTwo 4 where
  type PowerOf 4 = Lit 2
  getPower = speano

instance IsPowerOfTwo 8 where
  type PowerOf 8 = Lit 3
  getPower = speano

instance IsPowerOfTwo 16 where
  type PowerOf 16 = Lit 4
  getPower = speano

-- more powers go here

bSortN :: (IsPowerOfTwo n, Ord a) => OnVec n a
bSortN = fst $ genBitonicN getPower

Вот несколько примеров:

bSort1 :: Ord a => OnVec 1 a
bSort1 = bSortN

bSort2 :: Ord a => OnVec 2 a
bSort2 = bSortN

bSort4 :: Ord a => OnVec 4 a
bSort4 = bSortN

bSort8 :: Ord a => OnVec 8 a
bSort8 = bSortN

bSort16 :: Ord a => OnVec 16 a
bSort16 = bSortN

Я не знаю, можем ли мы избежать определения IsPowerOfTwo для каждой степени из двух.

Обновление: вот еще один вариант bSortN:

pnatToSPeano :: IPeano (Lit n) => proxy n -> SPeano (Lit n)
pnatToSPeano _ = speano

bSortNP :: (IPeano (Lit p), KnownPowersOfTwo (Lit p), Ord a)
        => proxy p -> OnVec (PowerOfTwo (Lit p)) a
bSortNP = fst . genBitonicN . pnatToSPeano

Пример:

bSort16 :: Ord a => OnVec 16 a
bSort16 = bSortNP (Proxy :: Proxy 4)