Replies: 3 comments
-
The big thing we lack in the type language is any way to do pattern matching that binds coercion variables; in Core this is just case expression. However, data families don't need this. When we have
we behave very much like
That is, we define a new, ordinary algebraic data type Then any use of Similarly pattern-matching on We'd need to do this in types too. But we need to be careful never to expose these |
Beta Was this translation helpful? Give feedback.
-
@goldfirere mentioned to me elsewhere that his comment about the need for coercion abstraction only applies if we take constraints into account. So it should be possible to promote simple data families. |
Beta Was this translation helpful? Give feedback.
-
This would go deliciously with an expansion of #106 to allow kind families, giving us open kinds without resorting to typo-vulnerable abuse of |
Beta Was this translation helpful? Give feedback.
-
At the moment, GHC does not support promotion of data families, as stated by the User’s Guide. See 6.4.10. Datatype promotion:
What exactly is missing to permit this? In #15245 @goldfirere says:
When does this arise? Could we promote some data families, but not all? In particular, here’s a data family that I’d like to promote:
In GHC 9.2.1, asking for the kind of
Tup3
gives me this error:My motivation comes from #281. To cite the proposal:
But it would be nicer to get this right from the get go. In particular, under
-XNoListTupleTypeSyntax
(part of the proposal), how do we print tuples? What should be the output ofToday the answer is
(Bool, Int)
. But that wouldn’t be the correct answer under-XNoListTupleTypeSyntax
! I would rather printTuple Bool Int
.And for a triple such as
(True, length [], 'x')
it could beTuple Bool Int Char
, and so on. If we could make theTuple
data family built-in, that would be possible. I’d also define it slightly differently to use built-in syntax:So the
Tup0
Tup1
Tup2
Tup3
constructors above are just to demonstrate the issue of promotion. In the final design I intend to go with the normal(a, b, c)
syntax.Q: Why not use a type family?
A: Class instances.
With a data family, we could define e.g.
I’d want
Tuple
to be usable anywhere the tuple type constructor is usable today, so that the transition would be seamless.Any thoughts on this, @goldfirere, @simonpj, @RyanGlScott, others? Could we support promotion of
Tuple
specifically if not all data families in general? And if so, could identify a set of restrictions that makes it possible?Beta Was this translation helpful? Give feedback.
All reactions