foreach - Haskell

foreach is actually a valid keyword. This code type-checks:

type T :: Type -> foreach (r :: Type) -> Type -> Type
data T k r a

type T' :: Type -> Type
type T' a = T a Identity a

https://gitlab.haskell.org/ghc/ghc/-/wikis/dependent-haskell#4-quantifiers

But why does it have to take Type -> Type (ie., Identity)? That's a puzzle to me ...

Uh, PEBKAC. foreach is just a type variable. Not a special keyword. At least not yet.

https://gitlab.haskell.org/ghc/ghc/-/wikis/dependent-haskell

forall (r :: Type) -> is an existing syntax though

Plus at type level, erasure doesn't really matter (it's runtime thing), so it wouldn't give you any advantage

In dependent Haskell it will matter though, to be able to write:

vReplicate :: foreach (n :: Nat) -> a -> Vec n a
vReplicate Zero     _ = Nil
vReplicate (Succ n) x = x :> vReplicate n x

The proposed syntax from that link:

                  ------------  Attribute ------------------
Quantifier        Dependence     Visibility     Erasure
------------------------------------------------------------
forall a. ty      Dependent      Invisible      Erased
forall a -> ty    Dependent      Visible        Erased
foreach a. ty     Dependent      Invisible      Retained
foreach a -> ty   Dependent      Visible        Retained
Eq a => ty        Non-dependent  Invisible      Retained
t1 -> t2          Non-dependent  Visible        Retained

Sridhar Ratnakumar said:

In dependent Haskell it will matter though, to be able to write:

vReplicate :: foreach (n :: Nat) -> a -> Vec n a
vReplicate Zero     _ = Nil
vReplicate (Succ n) x = x :> vReplicate n x

It will matter at value level - at type level (or kind level if you will), you're not concerned with erasure, because you can already match on type variables - e.g. in closed type families

E.g.

ghci> :{
ghci| type        Foo :: forall (t :: Type) -> t -> t
ghci| type family Foo t where
ghci|   Foo Type = Identity
ghci|   Foo (Type -> Type) = IdentityT
ghci| :}
ghci> :k! Foo Type
Foo Type :: * -> *
= Identity
ghci> :k! Foo (Type -> Type)
Foo (Type -> Type) :: (* -> *) -> * -> *
= IdentityT
ghci> :k! Foo _ Int
Foo _ Int :: *
= Identity Int
ghci> :k! Foo _ Maybe
Foo _ Maybe :: * -> *
= IdentityT Maybe

Basically, erasure doesn't make much sense here, because both types and kinds are evaluated "at the same time", while typechecking
You could probably interpret them in some staged way similar to typechecking vs. evaluation, but GHC doesn't do that AFAIK

Ah, yes. You were talking about at type-level (type-checking is always at compile-time; but erasure is a run-time thingy).

by the way, you can have ghci print Type in lieu of *, and do other cool things using some of these flags and extensions: https://github.com/srid/haskell-template/blob/master/haskell-template.cabal

Sridhar Ratnakumar said:

by the way, you can have ghci print Type in lieu of *, and do other cool things using some of these flags and extensions: https://github.com/srid/haskell-template/blob/master/haskell-template.cabal

Thanks - TBH I'm just lazy and don't have any top level GHCi config :big_smile:

Me neither; I just start ghci from that project, using nix develop -c cabal -- repl (or run https://github.com/srid/haskell-template/blob/master/bin/repl )