Jon Sterling3d ago

It's difficult to design a language that has implicit arguments *and* allows you to explicitly instantiate them. Agda has done very admirably.

But I do not like bound names, which are often single letters, getting undeservedly elevated to names that play a descriptive role.

My maxim is:

If you see {A = A} in an argument list, they blew it.

Show threadOwen Lynch
@jonmsterling This is a semi-related question: is it possible to check "generically" whether implicit arguments are inferable given that a function is applied to arguments with fully synthesized types? This could be a useful feature to have.
Jun 25 at 9:14amWeb
Show threadJon Sterling3d ago
@olynch That's a very interesting question. I'm not sure... it sounds kind of plausible though that something like this might be possible :)
Show threadNathaniel Burke3d ago

@olynch @jonmsterling

I think a conservative check would sometimes be too restrictive. Consider

bind : {M : Type -> Type} {A B : Type} -> Monad M -> (A -> M B) -> M A -> M B

In practice, this definition is usually fine because M will be instantiated with some (definitionally) injective type former like List, and problems like List ?B = List Int are solvable, but technically we could instantiate M with a constant family like \_. Nat, and now inferring B is hopeless. Having to make B an explicit arguments to bind, merely to defend against this edge-case, would kinda suck IMO...

Show threadOwen Lynch3d ago
@NathanielB @jonmsterling Interesting! Yeah makes sense that you'd need something like injectivity to make sense of this.
Show threadAndrasKovacs2d ago
@olynch @NathanielB @jonmsterling Haskell-style usage of typeclasses only supports reasonably strong and stable inference if there's a way to specify functions with definitionally injective application. "return True" infers "m Bool", where "Monad m", and if we check that against "Maybe Bool", we want to deduce "m = Maybe". So in a TT we should declare the Monad class with injective functions for the parameter. Practically this requires instances to be formal type constructors but not random functions.
Show threadConstantine Theocharis2d ago

@AndrasKovacs Would it make sense/be possible to have a dedicated ‘injective’ function space in the type system for this?

@olynch @NathanielB @jonmsterling

Show threadAndrasKovacs2d ago
@constantine @olynch @NathanielB @jonmsterling Yes, that's the proper way IMO.
Show threadOwen Lynch2d ago
@AndrasKovacs @constantine @NathanielB @jonmsterling OK neat; I wonder how this integrates with the approach to nominality via kinetic/potential elements (https://owenlynch.org/blog/nominal-types-via-energies/).
Nominal Types via Energies - Owen Lynch

Show threadJon Sterling2d ago
@olynch @AndrasKovacs @constantine @NathanielB Was wondering about this too.
Show threadJon Sterling2d ago
@AndrasKovacs @constantine @olynch @NathanielB Very curious about how this works…
Show threadConstantine Theocharis2d ago

@jonmsterling @AndrasKovacs @olynch @NathanielB i guess it is only introduced by type constructors and has an application rule (and no computation rules). You can wrap it in a normal lambda to recover the usual function space (and probably elaboration can do this automatically).

Though I wonder if it’s possible to do better..

Show threadZhixuan Yang2d ago
@constantine @jonmsterling @AndrasKovacs @olynch @NathanielB This proposal sounds similar to how GHC tracks injectivity of type-level functions, and GHC additionally allows the user to manually mark type-level functions as injective (and GHC checks it).
Show threadConstantine Theocharis2d ago

@zyang That suggests you could also have lambdas for this function space as long as the body is injective with respect to the bound variable.

@jonmsterling @AndrasKovacs @olynch @NathanielB

Show threadZhixuan Yang2d ago

@constantine @jonmsterling @AndrasKovacs @olynch @NathanielB Yes, the syntax for doing this in GHC is like

```
type family MyInjFun (a :: Type) = (result :: Type) | result -> a where
MyInjFun a = Maybe (Maybe a)
```
The syntax looks indeed rather unintuitive...

Show threadAndrasKovacs2d ago
@zyang @constantine @jonmsterling @olynch @NathanielB The system I have in mind is closer to the unsaturated type families proposal: https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0242-unsaturated-type-families.rst Currently we can't abstract over injective type families, we can only mark specific type families as injective.
ghc-proposals/proposals/0242-unsaturated-type-families.rst at master · ghc-proposals/ghc-proposals

Proposed compiler and language changes for GHC and GHC/Haskell - ghc-proposals/ghc-proposals

GitHub