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

Well formedness of Associated data type #33

Open
fxdpntthm opened this issue Apr 28, 2022 · 0 comments
Open

Well formedness of Associated data type #33

fxdpntthm opened this issue Apr 28, 2022 · 0 comments
Labels
Low Priority Things that are good to have but not needed question Further information is requested

Comments

@fxdpntthm
Copy link
Collaborator

fxdpntthm commented Apr 28, 2022

Currently we assign a mirror $wf:ATC to an associated type ATC of class say C.
or

class C  a where
   type ATC a 
   op :: ...

gets elaborated to

class C  a where
   type ATC a 
   type $wf:ATC a :: Constraint
   op :: ...

Will it be more appropriate to add the class constraint as the wellformedness mirror?

Possible problem may be that the associated data type has fewer type variables than the class variables potentially, giving rise to unambiguous types post elaboration.

Motivation:
There are cases where a data type references an associated type.

data IsNode a => Graph a = Graph { graphMap :: (Map (Key a) a) }

class Ord (Key a) => IsNode a where
  type Key a :: *
  nodeKey :: a -> Key a
  nodeNeighbors :: a -> [Key a]
@fxdpntthm fxdpntthm added question Further information is requested Low Priority Things that are good to have but not needed labels Apr 28, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Low Priority Things that are good to have but not needed question Further information is requested
Projects
None yet
Development

No branches or pull requests

1 participant