add modernized data-treify into package? #14
Comments
|
I've never heard of
|
|
The code i linked is my wip modernization of conals data-treify package.
Where I changed it to use ghcs modern typable apis. His has been in hackage
for a long time.
https://github.com/cartazio/data-treify-ng/blob/1d801af3826b5c74df399950bcd510ed710fc57a/src/Exp.hs
Is the example that Conal has included In the repo, suitably modernized
it’s intended to be used for doing observational sharing on typed asts, as
is the typical use case of gadts
Does it subsume non indexed data reify? That’s a good question. I’ll get
back to you on that
…On Thu, Feb 16, 2023 at 6:48 PM Ryan Scott ***@***.***> wrote:
I've never heard of data-treify before. I'm not necessarily opposed to
the idea of incorporating something like this into data-reify, but I
don't understand it well enough to say if this makes sense (or if this is
something that I could reasonably maintain). Some questions that come to
mind after glancing at the library:
1. Why did this code come to be? The .cabal file mentions that
data-reify was "tweaked it for typed syntax representations for use
with GADTs"
<https://github.com/cartazio/data-treify-ng/blob/1d801af3826b5c74df399950bcd510ed710fc57a/data-treify.cabal#L5>,
but it's not clear to me exactly what that means.
2. Is data-treify a strictly more powerful interface than what
data-reify offers? That is, does the former subsume the latter? Or are
they solving different problems?
3. What are some examples of actually using data-treify? The repo
doesn't include any examples, which leaves me wondering about how it's
actually put into practice. Having some examples or a test suite in
data-treify would help me a lot to contextualize where it sits in
relation to data-reify.
—
Reply to this email directly, view it on GitHub
<#14 (comment)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/AAABBQWYWWEJVUXNHISU3FTWX24D3ANCNFSM6AAAAAAU6YK74I>
.
You are receiving this because you authored the thread.Message ID:
***@***.***>
|
|
so heres an example where data-reify fails, thats a self contained file {-# LANGUAGE TypeFamilies, DeriveFunctor, DeriveFoldable, DeriveTraversable #-}
{-# LANGUAGE GADTs #-}
{-# OPTIONS_GHC -Wno-unused-imports #-}
module Main(main,Exp(..),ex1,ex2,ExpF(..)) where
import Control.Applicative
import Data.Reify
import Data.Traversable
import Data.IntMap as IntMap
import Data.Foldable
import Data.Monoid
import Type.Reflection
import Data.Type.Equality
import Data.Kind (Type)
main :: IO ()
main = print "indexed"
data Exp :: Type -> Type where
ETrue :: Exp Bool
EFalse :: Exp Bool
EFloat :: Float -> Exp Float
EEq :: Exp a -> Exp a -> Exp Bool
EAnd :: Exp Bool -> Exp Bool -> Exp Bool
EPlus :: Exp Float -> Exp Float -> Exp Float
data ExpF :: Type -> Type where
EFTrue :: ExpF a
EFFalse :: ExpF a
EFFloat :: Float -> ExpF a
EFEq :: ExpF a -> ExpF a -> ExpF a
EFAnd :: ExpF a -> ExpF a -> ExpF a
EFPlus :: ExpF a -> ExpF a -> ExpF a
ex1 :: Exp Float
ex1 = EFloat 1 `EPlus` EFloat 2
ex2 :: Exp Bool --- example of implicit sharing
ex2 = ex1 `EEq` ex1
instance MuRef (Exp i) where
type DeRef (Exp i) = ExpF
mapDeRef f x = case x of
ETrue -> pure EFTrue
EFalse -> pure EFFalse
EFloat x -> pure $ EFFloat x
EEq a b -> liftA2 EFEq (f a) (f b) with the error being |
|
Thanks for the examples! Before diving into the specifics of EEq :: Exp a -> Exp a -> Exp BoolI would have expected the corresponding data constructor in the EFEq :: a -> a -> ExpF a But instead, your example defines it as: EFEq :: ExpF a -> ExpF a -> ExpF aAs far as I can tell, this is the reason why the That being said, this doesn't seem like the full story. One thing that EEq :: ... -> Exp BoolThat is, where are indexing the return type by EFEq :: ... -> ExpF aIs this what you'd expect? I'm genuinely asking here, as I have no prior experience with the idioms of |
|
As far as whether It's interesting that the kind of This is all to say: I'm still not sure if I've fully understood all of the subtleties of what is going on in |
|
yup my example was wrong , i forgot to replace the recursive instances with the parameter |
|
i'll cleanup the indexed type example a little bit more and include it with the other now mostly buildable examples as a new PR. My conclusion so far (after you pointed out my mistake) is that "it looks like you can use data reify on typed syntax, but you'll wind up needing to do some sort of existential or runtime checks". So i think i can write something that roughly looks like
and then the conversion from the graph back to syntax would just be checking the indices one way or another, and a toplevel "sanity check" using the top level typeable instance. or something like that |
|
yeah, the example i have here is basically a forgetful functor/type erasure |
|
i guess this ticket is my misadventures in understanding how to use data-reify for typed syntax :) |
|
my example isn't a port of the Conal style "parameterized over variable rep and indexed by expression type" because It seems like it (the type indices in the conal one) require Existential wrapping like wrapping the "data-reifyed" sharing graph nodes |
|
I've had a chance to look at this code a little more closely, and one thing that I can't help but wonder is: why is class MuRef (h :: k -> Type) where
type DeRef h :: (k -> Type) -> k -> Type
mapDeRef :: forall m v. Applicative m
=> (forall a. h a -> m ( v a))
-> (forall a. h a -> m (DeRef h v a))This is much simpler, as now there is no need to make Similarly, I think we could simplify the machinery in data Graph (e :: k -> Type) =
Graph
[(Unique,Some (e (Const Unique)))]
UniqueWhere data Some :: (k -> Type) -> Type
Some :: f x -> Some fThe use of What do you think of this version, @cartazio? It's rather different from the original presentation in |
|
I like this design / idea! This actually seems like stab in the direction of a more principled api. (comparing some of the factoring in in the case of the Some, that would push any dictionary bits into the right hand side of i'm a teeny bit confused about your proposed the kind of |
Oops, that was a typo. I meant to write reifyGraph :: MuRef h => h a -> IO (Graph (DeRef h))
I'm not quite sure what you mean by "dictionary bits". Are you asking what happens when GADT constructors have constraints in their type? That is something that this version of data E :: (Type -> Type) -> Type -> Type where
Op :: Op a -> E v a
(:^) :: (Typeable a, Typeable b) =>
E v (a -> b) -> E v a -> E v b
data N :: (Type -> Type) -> Type -> Type where
ON :: Op a -> N v a
App :: (Typeable a, Typeable b) =>
v (a -> b) -> v a -> N v b
instance MuRef (E v) where
type DeRef (E v) = N
mapDeRef _ (Op o) = pure $ ON o
mapDeRef k (f :^ a) = App <$> k f <*> k aThe |
|
to be clear: i totally see that there shouldn't be a need for dictionaries in bottom up reconstruction, i'm just trying to make sure I see a clear way to get |
|
ok gotcha |
|
this looks nice! |
|
if the typeable dictionaries aren't needed, all the better! |
|
(like, would |
|
and without any unsafe trust me casts? (though that would be pretty safe i think) |
I'm not entirely sure. I presume that The only part that might be tricky to do without extract a' (Just (Bind (V _ a) n))
| Just Refl <- a `testEquality` a' = n
| otherwise = error "bindsF: wrong type"This is doing a type-safe cast using a |
|
i'm just poking at the in-tree example, not presupposing its authoritative, but I think you're right, that's the hard bit :) I"ll have a look see in a few days, I think the forgetful formulation will suffice for some of my near term stuff. |
|
i guess the lin extract a' (Just (Bind (V _ a) n))
| Just Refl <- a `testEquality` a' = n
| otherwise = error "bindsF: wrong type"really comes down to "you'll need something that provides an full error /Users/carter/WorkSpace/projects/active/data-treify-ng/src/Exp.hs: line 159, column 52:
error:
• Couldn't match type ‘a1’ with ‘a'’
Expected: n (V TypeRep) a'
Actual: n (V TypeRep) a1
‘a1’ is a rigid type variable bound by
a pattern with constructor:
Bind :: forall (f :: * -> *) (n :: (* -> *) -> * -> *) a.
Typeable a =>
V f a -> n (V f) a -> Bind f n,
in an equation for ‘extract’
at src/Exp.hs:158:22-35
‘a'’ is a rigid type variable bound by
the type signature for:
extract :: forall a'.
TypeRep a' -> Maybe (Bind TypeRep n) -> n (V TypeRep) a'
at src/Exp.hs:156:4-70
• In the expression: n
In an equation for ‘extract’:
extract a' (Just (Bind (V _ a) n))
| True = n
| otherwise = error "bindsF: wrong type"
In an equation for ‘bindsF’:
bindsF binds
= \ (V i' a') -> extract a' (I.lookup i' m)
where
m :: I.IntMap (Bind TypeRep n)
m = I.fromList [(i, b) | b@(Bind (V i _) _) <- binds]
extract :: TypeRep a' -> Maybe (Bind TypeRep n) -> n (V TypeRep) a'
extract _ Nothing = error "bindsF: variable not found"
extract a' (Just (Bind (V _ a) n))
| True = n
| otherwise = error "bindsF: wrong type"
• Relevant bindings include
n :: n (V TypeRep) a1 (bound at src/Exp.hs:158:35)
a :: TypeRep a1 (bound at src/Exp.hs:158:32)
a' :: TypeRep a' (bound at src/Exp.hs:158:12)
extract :: TypeRep a' -> Maybe (Bind TypeRep n) -> n (V TypeRep) a'
(bound at src/Exp.hs:157:4)
|
159 | | True {-Just Refl <- a `testEquality` a'-} = n
| ^ |
|
i'll have a go at trying your suggestions on data-treify and share what i learn. I suspect that something with constraint kinds might be needed, where we default to no class constraints .. or maybe just some uses push a typeable constraint on the instance like maybe i just need instance Typeable t => MuRef (f t) where |
https://github.com/cartazio/data-treify-ng/tree/main/src/Data I migrated Conals data Treify into using Data.Type.Equality and Type.Reflection, might be nice to make things a one stop shop once and for all?
thoughts: @andygill @RyanGlScott and others?
The text was updated successfully, but these errors were encountered: