Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.

`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
``````

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.

`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 )