Short critique about your AoH post.

Thanks for bringing this up! The most simple version of map that I can think of that works for vectors is this one

map :: (a -> b) -> Vec n a -> Vec n b
map f Nil = Nil
map f (x `Cons` xs) = (f x) `Cons` (map f xs)

which requires no scary types, foralls, rank 2 functions, or constraints! :D

The main thesis of the post was to describe the dependently typed fold as it is defined in the Clash library and the definition given in textbooks (for example, the ind-Vec function given in "The Little Typer", p. 248 and the original definition given by Conor McBride in his paper describing motive functions (sec 2.4)). Specifically, these definitions break out the motive function (the type level induction mentioned in the tweet), which helps show where the type level fold function comes into play versus where the value level function comes into play. In a subsequent post, I will be demonstrating how to use this definition of dfoldr (the one given in the Clash library) to generate circuits on an FPGA, such as the population counter example given in the dtfold documentation. Put another way, I wanted to help my Clash using friends understand the dfoldr function so they could use it in their FPGA designs.

If you would like, I could do one of the following.

Add a reference to the tweet describing other methods for defining the dependent fold in a footnote elaborating more on this specific point.
The code defined in the tweet could be incorporated into the article, with a credit statement referencing the origin of the code.

Or any other option that you think of that I haven't enumerated.

The main thesis of the post was to describe the dependently typed fold as it is defined in the Clash library

That should be in the introduction. Clash is a real world application (library), which imposes extra constraints. (I guess that e.g. using peano type level numbers will make it unusably slow for real world designs). It makes introductionary things more complicated, for not yet known or easily articulable reasons.

vmap can be written very simply, but your post is about writing map (and sum) with fold(s).

The defining the dependently typed fold on vectors section makes a very large jump. (like drawing an owl).

I tried to write dfoldr directly on Vec, and it's very much like list case (if you know simple answer, then it's simple).

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}

import Data.Type.Nat
import Data.Vec.Lazy (Vec (..))

dfoldr
    :: f 'Z
    -> (forall m. a -> f m -> f ('S m))
    -> Vec n a
    -> f n
dfoldr z _ VNil       = z
dfoldr z f (x ::: xs) = f x (dfoldr z f xs)

vmap :: (a -> b) -> Vec n a -> Vec n b
vmap f = getMapRes . dfoldr (MapRes VNil) (\x (MapRes xs) -> MapRes (f x ::: xs))

-- I encode motives as newtypes, it's in my opinion more straightforward.
newtype MapRes b n = MapRes { getMapRes :: Vec n b }

Decorating that function with SNats, KnownNats is optional. Also, using defunctionalization (Apply) is completely optional. (I prefer newtypes as a starting point - we use them elsewhere as well to make kinds align).

However, when you make type-level variables relevant in dfoldr, i..e add KnownNat-like constraints (dictionaries) nothing should really change. The SNatI from fin isn't good enough. We can have a better behaved but more complicated SNatJ though.

ddfoldr
    :: forall n a f. SNatJ n
    => f 'Z
    -> (forall m. SNatJ m => a -> f m -> f ('S m))
    -> Vec n a
    -> f n
ddfoldr z f = go where
    go :: SNatJ p => Vec p a -> f p
    go VNil       = z
    go (x ::: xs) = f x (go xs)

-- This is not how `fin` represents its "KnownNat", i.e. SNatI,
-- but encoding it this way makes ddfoldr definition simpler,
-- as matching on Vec cons case refines the constraint automatically.
type family SNatF (n :: Nat) :: Constraint where
    SNatF 'Z     = ()
    SNatF ('S n) = (SNatJ n, SNatI n)

class (SNatF n, SNatI n) => SNatJ (n :: Nat) where snatJ :: SNat n
instance            SNatJ 'Z     where snatJ = SZ
instance SNatJ n => SNatJ ('S n) where snatJ = SS

When you look at the type of ddfoldr

ddfoldr
    :: forall n a f. SNatJ n
    => f 'Z
    -> (forall m. SNatJ m => a -> f m -> f ('S m))
    -> Vec n a
    -> f n

you may notice that it's very close to

induction -- over natural numbers.
    :: forall n f. SNatJ n
    => f 'Z
    -> (forall m. SNatJ m => f m -> f ('S m))
    -> f n

Whether it makes sense to implement ddfoldr using induction, depends.

However the idea of writing functions for Vec using induction is good to know:

I know how to map empty vectors
I know how to map vectors of size (n + 1) when I know how to map vectors of size n
Induction: I know how to map vectors.

I think that is in fact very useful, as many functions fall into that pattern. (e.g. vrepeat, vpure :: a -> Vec n a isn't implementable with dfoldr, but is with induction).

Thanks for writing the post. I wouldn't thought about SNatJ variant, and whether I should add it to fin lib.

What could fit your narrative better, is to proceed from "my" simple dfoldr to Clash dfold with a note that added stuff (KnownNat/SNat, defunctionlization) will prove itself useful in the future (post),, but isn't really necessary for something simple as implementing vmap.

Important note: the motive in Clash' dfold is a motive for natural number induction! Motive for induction over Vec would be something like

vecInd
    :: (forall n a (xs :: Vec n a) -> Type)
    -> ...

so even Clash' dfold doesn't match KnownNat k (but learns what k is from the structure of the Vec argument), morally it does (induction on k).

dfold :: forall p k a . KnownNat k
      => Proxy (p :: TyFun Nat Type -> Type)                      -- ^ The /motive/
      -> (forall l . SNat l -> a -> (p @@ l) -> (p @@ (l + 1)))   -- ^ Succ case
      -> (p @@ 0)                                                 -- ^ Initial element
      -> Vec k a                                                  -- ^ Vector to fold over
      -> (p @@ k)

So given your follow-up plans, I think you could make it clearer that you explaining how Clash does dependent-typing things. As I have shown, without their concerns (whatever they are to scale to real circuits), it can be simpler.

The "dependent-types" programming in Haskell is not really as complicated as your post might imply. E.g. one don't strictly need defunctionalization here. Unfortunately, the SNatJ I introduce is complicated, luckily it can be part of a library.

ryanorendorff / ryanorendorff.github.io

Short critique about your AoH post. #3