3 ms·
He used pseudo-notation for something that is possible in GHC. (1+) on type level corresponds to the successor function, and a compiling version of Peaker's cod
by quchen 13y ago
He used pseudo-notation for something that is possible in GHC. (1+) on type level corresponds to the successor function, and a compiling version of Peaker's code would be this:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
data Nat = Z | S Nat
data Vector l a where
Nil :: Vector Z a
Cons :: a -> Vector l a -> Vector (S l) a
- jdn 13y agoThanks for this! Had looked at examples of this but it's nice to have the link to Peaker's code