Opened 21 months ago

Last modified 21 months ago

#11387 new feature request

Typecasting using type application syntax

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Compiler Version:
Keywords: TypeApplications Cc: adamgundry
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: #11350 Differential Rev(s):
Wiki Page:

Description

I created #11350 to allow visible (static) type applications in patterns. I had a thought about translating non-parametric type applications in patterns as a runtime type check (Typeable) and decided to create a ticket in case it made any sense. Example:

doubleWhenInt :: forall a. Typeable a => a -> a
doubleWhenInt x =
  case eqT @Int @a of
    Just Refl -> x + x
    Nothing   -> x

-- Becomes…
doubleWhenInt :: Typeable a => a -> a
doubleWhenInt @Int n = n + n
doubleWhenInt @_   x = x

Thoughts?

Change History (3)

comment:1 Changed 21 months ago by adamgundry

Cc: adamgundry added

It would make sense to do something a bit like this.

If a :: * is a type, then a Typeable a constraint is essentially an (invisible) singleton witness to a; the visible singleton is TypeRep a. I think the Right Thing to do would be to get rid of the singleton construction and add pi-types, so that we have

doubleWhenInt :: pi a . a -> a
doubleWhenInt @Int n = n + n
doubleWhenInt @_   x = x

The pi a . quantifier corresponds to forall a . Typeable a =>. The type argument is operationally relevant, can be pattern-matched and hence is non-parametric. The argument would be invisible-by-default (e.g. you might write doubleWhenInt True at a call site) but could be made visible like other type arguments (e.g. doubleWhenInt @Int 42 should be allowed).

(It's not completely obvious whether arguments to pi-quantified functions should be in the type namespace or the term namespace, because they exist at both levels.)

comment:2 Changed 21 months ago by goldfire

Yes, this is sensible, but I prefer Adam's construction. Yes, the namespace issue is thorny. No, I don't have plans to implement this today. I believe this will be much easier to do after we have pi for non-*-kinded things.

comment:3 Changed 21 months ago by rwbarton

For one thing, pi quantifiers would come in a specific order, while Typeable constraints live in a bag of constraints. What would happen if you have multiple types to match on?

Note: See TracTickets for help on using tickets.