purescript / purescript-typelevel-prelude

Types and kinds for basic type-level programming
BSD 3-Clause "New" or "Revised" License
63 stars 21 forks source link

Add Homogeneous and HomogeneousRowList for homogeneous rows #20

Closed paulyoung closed 6 years ago

paulyoung commented 7 years ago

This is my first attempt at type-level programming. Hopefully it's pretty self explanatory, but the idea is to make sure that every field in a record has the same type.

Something similar can be achieved using StrMap, but it's not quite the same.

This initial version is available to play with at http://try.purescript.org/?gist=bec330aab7a6c0b21e466e37483dfba9. It was originally adapted from http://try.purescript.org/?gist=2720825b0476c8924717437fb6f6eefb.

I think it would be great to support polymorphism and open rows, but I haven't had any success with that.

Any and all feedback is welcome.

paf31 commented 7 years ago

Looks good, thanks! A few notes though:

LiamGoodacre commented 7 years ago

@paf31 is the motivation for the TypeEquals approach, that you get a nicer error and don't see the RowList implementation artifact?

paf31 commented 7 years ago

Yes, since the type is already determined if the fundep is added anyway.

paulyoung commented 7 years ago

Thanks for the feedback so far. Good call on moving this to Row.

Here's what I have so far:

class Homogeneous row fieldType
instance homogeneous
  :: ( RowToList row fields
     , FieldOf fields fieldType
     )
  => Homogeneous (? row) fieldType -- not sure what to do here

class FieldOf (rowList :: RowList) fieldType
instance fieldOfCons
  :: (FieldOf tail fieldType)
  => FieldOf (Cons symbol fieldType tail) fieldType
instance fieldOfNil :: FieldOf Nil fieldType

Does this seems like I'm on the right track?

I'm not quite sure about the other 2 bullet points but eager to understand.

LiamGoodacre commented 7 years ago

@paulyoung The Homogeneous type class will need a kind annotation of # Type on the row parameter. For the instance, all the arguments can be left as type variables. I.e:

instance homogeneous
  :: ( RowToList row fields
     , FieldOf fields fieldType
     )
  => Homogeneous row fieldType

Phil's point about TypeEquals is referring to the FieldOf (Cons symbol fieldType tail) fieldType instance. The fieldType appears twice across multiple instance arguments. This isn't necessarily bad, it's just that if there is a mismatch the error will mention that it couldn't find an instance for FieldOf .... We'd rather have an error that two types weren't equal. So the action here is to rename one of the two usages of fieldType and add a new instance constraint requiring that those two types be equal.

The functional dependencies for FieldOf should be | rowList -> fieldType. Because once we know which instance to select - which we do by looking at the rowList, i.e whether or not it is Nil or Cons - and the constraints have been satisfied, the fieldType should be fully determined. The same sort of functional dependencies could be used on Homogeneous.

For future reading, the following is incorrect. If you require multiple constraints with the same type class they will conflict and give you overlapping instances.

In cases where there is only one instance with all the arguments being type variables, I usually have both parameters always determined | -> row fieldType - but I think Phil sometimes disagrees with doing that? @paf31

paf31 commented 7 years ago

I don't think we can have both parameters determined, since that says you can predict the row given no information.

paulyoung commented 7 years ago

Thanks for the helpful feedback so far. I pushed some changes.

paulyoung commented 7 years ago

Is there anything else I can do here?

paf31 commented 7 years ago

@LiamGoodacre Any thoughts on this? What do you think about creating some submodules here?

LiamGoodacre commented 7 years ago

Just been thinking about the fundeps and I'm thinking that this might suffer from the same issue I mentioned about multiple constraints. I'll try to come up with a demonstration tonight.

LiamGoodacre commented 7 years ago

Actually, I am mistaken. Ignore my previous concern.

LiamGoodacre commented 7 years ago

Submodules sound good. What do you suggest here? @paf31

paulyoung commented 6 years ago

Should I put this in a Type.Row.Homogeneous module?

paf31 commented 6 years ago

Should I put this in a Type.Row.Homogeneous module?

Sorry for the delay. Yes please.

paulyoung commented 6 years ago

I think I've addressed everything in the latest round of feedback.

paf31 commented 6 years ago

Thanks!