Language.Syntactic.Sharing.ReifyHO

This module is similar to Language.Syntactic.Sharing.Reify, but operates on HOAST rather than a general AST. The reason for having this module is that when using HOAST, it is important to do simultaneous sharing analysis and HOLambda reification. Obviously we cannot do sharing analysis first (using reifyGraph from Language.Syntactic.Sharing.Reify), since it needs to be able to look inside HOLambda. On the other hand, if we did HOLambda reification first (using reify), we would destroy the sharing.

This module is based on Type-Safe Observable Sharing in Haskell (Andy Gill, Haskell Symposium, 2009).

Documentation

reifyGraphTop :: Typeable a => (forall a. HOASTF ctx dom a -> Maybe (Witness' ctx a)) -> HOASTF ctx dom a -> IO (ASG ctx (Lambda ctx :+: (Variable ctx :+: dom)) a, VarId)

Convert a syntax tree to a sharing-preserving graph

reifyGraph

Arguments

:: Reifiable ctx a dom internal

=> (forall a. HOASTF ctx dom a -> Maybe (Witness' ctx a))

A function that decides whether a given node can be shared. Nothing means "don't share"; Just means "share". Nodes whose result type fulfills (Sat ctx a) can be shared, which is why the function returns a Witness'.

-> a

-> IO (ASG ctx (Lambda ctx :+: (Variable ctx :+: dom)) (NAryEval internal), VarId)

Reifying an n-ary syntactic function to a sharing-preserving graph

This function is not referentially transparent (hence the IO). However, it is well-behaved in the sense that the worst thing that could happen is that sharing is lost. It is not possible to get false sharing.