4 ms·
I'm not quite sure what you've done there. You seem to be confusing type signatures with function definitions. You've also used GADT syntax, requiring -XGADTs,
by jdn 13y ago
I'm not quite sure what you've done there. You seem to be confusing type signatures with function definitions. You've also used GADT syntax, requiring -XGADTs, which isn't needed for a simple vector type.
> Cons :: a -> Vector n a --> Vector (1 + n) a
This makes no sense, you can't specify constants in a type signature, and you certainly can't add constants to a type variable in one.
I may be the one not in the know here, if so please show me this magic.
- klibertp 13y agoNot in Haskell, but there are languages where it's possible. It's called dependent typing and I don't really understand how it works, but I suppose gp was referring to this.
- jdn 13y agoOh of course, and that also explains the use of GADTs since they are one route to dependent types in Haskell. I'm not sure what he's done there is fully legit, but maybe not as loony as at first thought.
- tel 13y agoIt plays fast and loose on notation, but is perfectly kosher in GHC (not Haskell2010 or Haskell98).
- sold 13y agoIt is possible in GHC, see parent comment.
- quchen 13y agoHe 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