Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add named field construction #16

Merged
merged 2 commits into from
Oct 19, 2019
Merged

Add named field construction #16

merged 2 commits into from
Oct 19, 2019

Conversation

i-am-tom
Copy link
Owner

The named library seems to make a lot of this look much prettier, so I'm very excited about this change!

Hoping @neongreen can give this change a quick look before I commit it to master :)

@i-am-tom
Copy link
Owner Author

Ah, need to fix the docs...

The `named` library seems to make a lot of this look much prettier, so
I'm very excited about this change!
instance Append (S1 m h) t (S1 m h :*: t)
instance Append x y z => Append (w :*: x) y (w :*: z)

class Rearrange (i :: Type -> Type) (o :: Type -> Type) | i -> o

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why is this a class if it has no methods? Shouldn't it be a type family?

type family Rearrange (i :: Type -> Type) = (o :: Type -> Type) where
  ...

Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

👍

import GHC.Generics
import Named ((:!), NamedF (..))

class Append (xs :: Type -> Type) (ys :: Type -> Type) (zs :: Type -> Type)

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why is this a class if it has no methods? Shouldn't it be a type family?

type family Append (xs :: Type -> Type) (ys :: Type -> Type) = (zs :: Type -> Type) where
  ...

Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good point; I think I'd set off with the intention of making this much more interestingly injective, but got lazy a bit too quick 😅

--
-- >>> :{
-- data User
-- = User { name :: String, age :: Int, likesDogs :: Bool }

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Shouldn't the example use fields of the same type but with different names to follow the motivation above?

Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good point, probably clearer!

-- ... standing for ...("name" :! f [Char])
-- ... -> ("age" :! f Int) -> ("likesDogs" :! f Bool) -> HKD User f...
-- ...
class Record (structure :: Type) (f :: Type -> Type) (k :: Type)

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The third parameter here can be replaced with an associated type.

Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The errors are never as useful, though :/

I'd be interested in exploiting some stuckness eventually to have an error if one forgets the type application, but it's probably out-of-scope for this change, so I'll leave it as-is :)

grecord fill = \(Arg inner) -> fill (M1 (K1 inner))

instance (GRecord right f structure k, rec ~ Rec0 x)
=> GRecord (S1 ('MetaSel ('Just name) i d c) rec :*: right) f structure (name :! x -> k) where

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There's no other instance matching on :*:, so better type errors / type inference is possible if the instance is defined as

left ~ ... => GRecord (left :*: right) f structure ...

Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Quite right; I'd intended for this behaviour to be introduced straight to Build.hs for any named-field record, but (having discussed with @kcsongor) the generic-lens upcasting doesn't work with unnamed fields yet, so it got split out. Good spot - I hadn't gone back and tidied up carefully enough 😇

@int-index
Copy link

int-index commented Sep 28, 2019

In general, this looks great, thanks for taking the time to make higgledy work with named! I left a few suggestions based on my belief that type families are slightly nicer than functional dependencies for type-level computation, but these suggestions are all minor and safe to ignore.

@@ -72,7 +75,7 @@ data User
deriving (Generic, Show)

user :: User
user = User "Tom" 25 True
user = User "Tom" 26 True

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

🙂

README.md Outdated
@@ -184,13 +187,30 @@ eg7 = eg6 [1] [] ["Tom", "Tim"]
-- Triple [1] [] ["Tom","Tim"]
```

Should we need to work with records, we can exploit the label trickery of the
[`named`](http://hackage.haskell.org/package/named) package. The `record`

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
[`named`](http://hackage.haskell.org/package/named) package. The `record`
[`named`](https://hackage.haskell.org/package/named) package. The `record`

README.md Outdated
eg8 = record @User

eg9 :: HKD User Maybe
eg9 = eg8 ! #name (Just "Tom") ! #likesDogs (Just True) ! #age (Just 26)

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Perhaps break this into several lines?

Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

👍

Copy link
Owner Author

@i-am-tom i-am-tom left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks so much @int-index for taking a look, some really great spots :) I'll commit, push, bump versions, and close up!

import GHC.Generics
import Named ((:!), NamedF (..))

class Append (xs :: Type -> Type) (ys :: Type -> Type) (zs :: Type -> Type)
Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good point; I think I'd set off with the intention of making this much more interestingly injective, but got lazy a bit too quick 😅

instance Append (S1 m h) t (S1 m h :*: t)
instance Append x y z => Append (w :*: x) y (w :*: z)

class Rearrange (i :: Type -> Type) (o :: Type -> Type) | i -> o
Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

👍

--
-- >>> :{
-- data User
-- = User { name :: String, age :: Int, likesDogs :: Bool }
Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good point, probably clearer!

-- ... standing for ...("name" :! f [Char])
-- ... -> ("age" :! f Int) -> ("likesDogs" :! f Bool) -> HKD User f...
-- ...
class Record (structure :: Type) (f :: Type -> Type) (k :: Type)
Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The errors are never as useful, though :/

I'd be interested in exploiting some stuckness eventually to have an error if one forgets the type application, but it's probably out-of-scope for this change, so I'll leave it as-is :)

grecord fill = \(Arg inner) -> fill (M1 (K1 inner))

instance (GRecord right f structure k, rec ~ Rec0 x)
=> GRecord (S1 ('MetaSel ('Just name) i d c) rec :*: right) f structure (name :! x -> k) where
Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Quite right; I'd intended for this behaviour to be introduced straight to Build.hs for any named-field record, but (having discussed with @kcsongor) the generic-lens upcasting doesn't work with unnamed fields yet, so it got split out. Good spot - I hadn't gone back and tidied up carefully enough 😇

@neongreen
Copy link

@i-am-tom ping

@i-am-tom i-am-tom merged commit e3b2cc2 into master Oct 19, 2019
@i-am-tom i-am-tom deleted the named branch October 19, 2019 17:09
@neongreen
Copy link

Thanks!

Can you also ping me when a new version is up on Hackage?

@i-am-tom
Copy link
Owner Author

i-am-tom commented Oct 21, 2019

Ping :)

Thanks so much for your incredible patience - it has been a hectic few weeks, and your nudges are appreciated!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants