------------ 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
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
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
foreach
is actually a valid keyword. This code type-checks: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 thoughPlus 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:
The proposed syntax from that link:
Sridhar Ratnakumar said:
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.
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.cabalSridhar Ratnakumar said:
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 )