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 Immutable type family #34

Closed
aavogt opened this Issue Jul 8, 2014 · 21 comments

Comments

Projects
None yet
5 participants
@aavogt
Copy link

aavogt commented Jul 8, 2014

type family Mutable is injective, but ghc doesn't know this. The inverse could be called

type family Immutable (m :: * -> * -> *) :: * -> *
type instance Immutable MVector = Vector -- for all the Storable, Unboxed etc.

If we instead had

unsafeFreeze :: (Immutable (Mutable v) ~ v, PrimMonad m, Vector v a)
  => Mutable v (PrimState m) a -> m (v a)

This function can then be written and the intermediate immutable vector type will not be ambiguous:

f v = convert `fmap` unsafeFreeze v
@cartazio

This comment has been minimized.

Copy link
Member

cartazio commented Jul 8, 2014

i'd support adding an Immutable type family

@cartazio

This comment has been minimized.

Copy link
Member

cartazio commented Jul 8, 2014

Q: why not (v~Immutable mv, mv~Mutable v) instead of the composition?

@cartazio

This comment has been minimized.

Copy link
Member

cartazio commented Feb 1, 2015

this should happen for 0.11

@aavogt

This comment has been minimized.

Copy link

aavogt commented Feb 1, 2015

FYI this construction doesn't help with ghc-7.10-RC2 https://ghc.haskell.org/trac/ghc/ticket/10009, but hopefully they fix it for 7.10.1

@jstolarek

This comment has been minimized.

Copy link
Contributor

jstolarek commented Feb 17, 2015

FWIW on my GHC branch with injective type families it is possible to declare Mutable as injective and the type of Adam's f function becomes unambiguous. You just have to wait until GHC 7.12 :-)

@jstolarek

This comment has been minimized.

Copy link
Contributor

jstolarek commented May 19, 2015

Aside: is there any reason why you don't use a data family here? That would be injective.

@aavogt

This comment has been minimized.

Copy link

aavogt commented May 19, 2015

@jstolarek data families don't play well with Data.Coerce.coerce. See https://gist.github.com/aavogt/936b03b8a7875e690649 . But maybe that's not a big deal

@aavogt

This comment has been minimized.

Copy link

aavogt commented May 19, 2015

nevermind it's not a problem for a newtype instance

@cartazio

This comment has been minimized.

Copy link
Member

cartazio commented May 19, 2015

If you have concrete design suggestion, please share them on the PR related
to this issue.

On Tuesday, May 19, 2015, Adam Vogt notifications@github.com wrote:

nevermind it's not a problem for a newtype instance


Reply to this email directly or view it on GitHub
#34 (comment).

@aavogt

This comment has been minimized.

Copy link

aavogt commented May 19, 2015

master...aavogt:mvector_data_family is the idea, but maybe modules could be rearranged so that no operations are (publicly) done with MVectorT

@jstolarek

This comment has been minimized.

Copy link
Contributor

jstolarek commented May 20, 2015

If you have concrete design suggestion, please share them on the PR related
to this issue.

Not a suggestion, rather a question of why a particular design choice was made. Anyway, if data families turn out not be an option then you can just wait until injectivity is available in GHC. The fix will be a one-liner (tested on a development branch).

@cartazio

This comment has been minimized.

Copy link
Member

cartazio commented May 20, 2015

I think at least for vector, injective type families won't be an option
till its in all the supported ghc versions, but once that happens, agreed.

On Wednesday, May 20, 2015, Jan Stolarek notifications@github.com wrote:

If you have concrete design suggestion, please share them on the PR related
to this issue.

Not a suggestion, rather a question of why a particular design choice was
made. Anyway, if data families turn out not be an option then you can just
wait until injectivity is available in GHC. The fix will be a one-liner
(tested on a development branch).


Reply to this email directly or view it on GitHub
#34 (comment).

@cartazio

This comment has been minimized.

Copy link
Member

cartazio commented May 27, 2015

@jstolarek @aavogt i kinda did one data family style approach (albeit not quite the one i think you mean) over hear https://github.com/wellposed/numerical/blob/bf0f50ad21f54a543da8948d3429f3d343cd4bbc/src/Numerical/Array/Storage.hs

I'm not sure if the data family approach makes sense (or at least i'm not understanding how it'd give the right UX), though injective families should certainly be the roadmap at some point because the vector mutable/immutable relationship is the poster child for injective time families

@RyanGlScott

This comment has been minimized.

Copy link
Member

RyanGlScott commented Jun 19, 2016

What's the current state of this issue? GHC 8.0 is out with support for TypeFamilyDependencies, and it's quite easy to make this change:

diff --git a/Data/Vector/Generic/Base.hs b/Data/Vector/Generic/Base.hs
index a760329..15f1a98 100644
--- a/Data/Vector/Generic/Base.hs
+++ b/Data/Vector/Generic/Base.hs
@@ -1,5 +1,10 @@
-{-# LANGUAGE Rank2Types, MultiParamTypeClasses, FlexibleContexts,
+{-# LANGUAGE CPP, Rank2Types, MultiParamTypeClasses, FlexibleContexts,
              TypeFamilies, ScopedTypeVariables, BangPatterns #-}
+
+#if __GLASGOW_HASKELL__ >= 800
+{-# LANGUAGE TypeFamilyDependencies #-}
+#endif
+
 {-# OPTIONS_HADDOCK hide #-}

 -- |
@@ -26,7 +31,12 @@ import Control.Monad.Primitive
 -- | @Mutable v s a@ is the mutable version of the pure vector type @v a@ with
 -- the state token @s@
 --
-type family Mutable (v :: * -> *) :: * -> * -> *
+type family Mutable (v :: * -> *)
+#if __GLASGOW_HASKELL__ >= 800
+                                  = (r :: * -> * -> *) | r -> v
+#else
+                                  :: * -> * -> *
+#endif

 -- | Class of immutable vectors. Every immutable vector is associated with its
 -- mutable version through the 'Mutable' type family. Methods of this class

such that @aavogt's unsafeFreeze example will typecheck:

unsafeFreeze :: (PrimMonad m, Vector v a) => Mutable v (PrimState m) a -> m (v a)
@aavogt

This comment has been minimized.

Copy link

aavogt commented Jun 19, 2016

@RyanGlScott looks good.

A silly reason to hold back is that people may write code that typechecks with ghc 8 but confusingly fails on ghc 7.10 and earlier.

@cartazio

This comment has been minimized.

Copy link
Member

cartazio commented Jun 19, 2016

Ooo. Yay!
I forgot about this. But yeah this is exactly something that will work
with injective type families today

(though sadly injective type families today only work for this and
equivalents and not for fun things like type level addition being semi
invertible as long as at least one of the two args is know. But that's not
relevant to this discussion )

On Sunday, June 19, 2016, Adam Vogt notifications@github.com wrote:

@RyanGlScott https://github.com/RyanGlScott looks good.

A silly reason to hold back is that people may write code that typechecks
with ghc 8 but confusingly fails on ghc 7.10 and earlier.


You are receiving this because you commented.
Reply to this email directly, view it on GitHub
#34 (comment), or mute
the thread
https://github.com/notifications/unsubscribe/AAAQwjvAcjk_v1ljk0fopHyAaGrsTyA9ks5qNW1YgaJpZM4CK_cz
.

@dolio

This comment has been minimized.

Copy link
Contributor

dolio commented Jul 23, 2016

Is the type checking thing really a "silly reason"?

Certainly GHC breaks type checking sometimes. But here it is kind of a second order consequence. We will have created something that doesn't work on all supported GHC versions, so depending on particular versions of vector will not be sufficient to ensure building; only specific GHC versions can ensure that the vector stuff happens to work.

What are people's thoughts on this?

@RyanGlScott

This comment has been minimized.

Copy link
Member

RyanGlScott commented Jul 23, 2016

depending on particular versions of vector will not be sufficient to ensure building; only specific GHC versions can ensure that the vector stuff happens to work.

Isn't this already the case? For example, we currently only define an IsList instance for Vectors if we're compiling against GHC 7.8 or later. This doesn't seem like a problem to me. After all, IsList is a GHC-specific extension, so the onus is on GHC programmers to make sure they're using a recent-enough GHC to do whatever trickery they want to do. The same argument can be applied to making Mutable injective.

As long as the documentation for Mutable advertises that it's injective if using GHC 8.0 or later, I'd be happy.

@dolio

This comment has been minimized.

Copy link
Contributor

dolio commented Jul 24, 2016

To me, that's a different scenario. It's GHC/base changing its API between 7.6 and 7.8. It has nothing to do with vector, we just support the new API if it exists. And depending on a specific version of base is required to use the API, because that's where it lives.

Immutable is an API vector provides that will only work correctly (in some scenarios) if you also depend on a specific base/GHC. It would (in some ways) be like conditionally defining a function in vector (or chaging its behavior) based on GHC version. I think we don't do things like that currently.

It's probably not a big deal. It's just slightly odd.

@cartazio

This comment has been minimized.

Copy link
Member

cartazio commented Jul 24, 2016

i'm not sure how mature injective type families are, but we should try to have something related to this for 0.12, or at least make some conclusions on that matter

@RyanGlScott

This comment has been minimized.

Copy link
Member

RyanGlScott commented Aug 20, 2017

Fixed in #160.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment