initial pass at structural hashing of data declaration cycles

parser-typechecker/src/Unison/ABT.hs

@@ -320,6 +320,16 @@ unabs t = ([], t)
 reabs :: Ord v => [v] -> Term f v () -> Term f v ()
 reabs vs t = foldr abs t vs
 
+transform :: (Ord v, Foldable g, Functor f)
+          => (forall a. f a -> g a) -> Term f v a -> Term g v a
+transform f tm = case (out tm) of
+  Var v -> annotatedVar (annotation tm) v
+  Abs v body -> abs' (annotation tm) v (transform f body)
+  Tm subterms ->
+    let subterms' = fmap (transform f) subterms
+    in tm' (annotation tm) (f subterms')
+  Cycle body -> cycle' (annotation tm) (transform f body)
+
 instance (Foldable f, Functor f, Eq1 f, Eq a, Var v) => Eq (Term f v a) where
   -- alpha equivalence, works by renaming any aligned Abs ctors to use a common fresh variable
   t1 == t2 = annotation t1 == annotation t2 && go (out t1) (out t2) where

parser-typechecker/src/Unison/DataDeclaration.hs

@@ -5,10 +5,72 @@
 
 module Unison.DataDeclaration where
 
+import Prelude hiding (cycle)
 import Unison.Type (Type)
-import GHC.Generics
+import qualified Unison.Type as Type
+import Unison.ABT (absChain, cycle)
+import Unison.Var (Var)
+import Unison.Hashable (Accumulate, Hashable1)
+import qualified Unison.Hashable as Hashable
+import qualified Unison.ABT as ABT
 
 data DataDeclaration v = DataDeclaration {
   bound :: [v],
-  constructors :: [(v, [Type v])]
+  constructors :: [(v, Type v)]
 } deriving (Show)
+
+-- type List a = Nil | Cons a (List a)
+-- cycle (abs "List" (LetRec [abs "a" (cycle (absChain ["Nil","Cons"] (Constructors [List a, a -> List a -> List a])))] "List"))
+-- absChain [a] (cycle ())"List")
+
+data F a
+  = Type (Type.F a)
+  | LetRec [a] a
+  | Constructors [a]
+  deriving (Functor, Foldable)
+
+instance Hashable1 F where
+  hash1 hashCycle hash e =
+    let (tag, hashed) = (Hashable.Tag, Hashable.Hashed)
+      -- Note: start each layer with leading `2` byte, to avoid collisions with
+      -- terms, which start each layer with leading `1`. See `Hashable1 Term.F`
+    in Hashable.accumulate $ tag 2 : case e of
+      Type t -> [tag 0, hashed $ Hashable.hash1 hashCycle hash t]
+      LetRec bindings body ->
+        let (hashes, hash') = hashCycle bindings
+        in [tag 1] ++ map hashed hashes ++ [hashed $ hash' body]
+      Constructors cs ->
+        let (hashes, _) = hashCycle cs
+        in [tag 2] ++ map hashed hashes
+
+{-
+  type UpDown = Up | Down
+
+  type List a = Nil | Cons a (List a)
+
+  type Ping p = Ping (Pong p)
+  type Pong p = Pong (Ping p)
+
+  type Foo a f = Foo Int (Bar a)
+  type Bar a f = Bar Long (Foo a)
+-}
+
+hash :: (Eq v, Var v, Ord h, Accumulate h)
+     => [(v, DataDeclaration v)] -> [(v, h)]
+hash recursiveDecls = zip (fst <$> recursiveDecls) hashes where
+  hashes = ABT.hash <$> toLetRec recursiveDecls
+
+toLetRec :: Ord v => [(v, DataDeclaration v)] -> [ABT.Term F v ()]
+toLetRec decls =
+  do1 <$> vs
+  where
+    vs = fst <$> decls
+    decls' = toABT . snd <$> decls
+    -- we duplicate this letrec once (`do1`) for each of the mutually recursive types
+    do1 v = cycle (absChain vs . ABT.tm $ LetRec decls' (ABT.var v))
+
+toABT :: Ord v => DataDeclaration v -> ABT.Term F v ()
+toABT (DataDeclaration bound constructors) =
+  absChain bound (cycle (absChain (fst <$> constructors)
+                                  (ABT.tm $ Constructors stuff)))
+  where stuff = ABT.transform Type . snd <$> constructors

parser-typechecker/src/Unison/FileParser.hs

@@ -20,6 +20,7 @@ import qualified Text.Parsec.Layout as L
 import qualified Unison.Parser
 import qualified Unison.Parsers as Parsers
 import qualified Unison.Term as Term
+import qualified Unison.Type as Type
 import qualified Unison.TermParser as TermParser
 import qualified Unison.TypeParser as TypeParser
 import Control.Monad.Reader
@@ -76,12 +77,17 @@ dataDeclaration = traced "data declaration" $ do
   (name, typeArgs) <- --L.withoutLayout "type introduction" $
     (,) <$> TermParser.prefixVar <*> traced "many prefixVar" (many TermParser.prefixVar)
   traced "=" . token_ $ string "="
+  -- dataConstructorTyp gives the type of the constructor, given the types of
+  -- the constructor arguments, e.g. Cons becomes forall a . a -> List a -> List a
+  let dataConstructorTyp ctorArgs =
+        Type.foralls typeArgs $ Type.arrows ctorArgs (Type.apps (Type.var name) (Type.var <$> typeArgs))
+      dataConstructor =
+        (,) <$> TermParser.prefixVar
+            <*> (dataConstructorTyp <$> many TypeParser.valueTypeLeaf)
   traced "vblock" $ L.vblockIncrement $ do
     constructors <- traced "constructors" $ sepBy (token_ $ string "|") dataConstructor
     pure $ (name, DataDeclaration typeArgs constructors)
-  where
-    dataConstructor = traced "data contructor" $ (,) <$> TermParser.prefixVar
-                          <*> (traced "many typeLeaf" $ many TypeParser.valueTypeLeaf)
+
 
 effectDeclaration :: Var v => Parser (S v) (v, EffectDeclaration v)
 effectDeclaration = traced "effect declaration" $ do

parser-typechecker/src/Unison/Type.hs

@@ -147,6 +147,9 @@ ann e t = ABT.tm (Ann e t)
 forall :: Ord v => v -> Type v -> Type v
 forall v body = ABT.tm (Forall (ABT.abs v body))
 
+var :: Ord v => v -> Type v
+var = ABT.var
+
 existential :: Ord v => v -> Type (TypeVar v)
 existential v = ABT.var (TypeVar.Existential v)
 
@@ -159,6 +162,12 @@ v' s = ABT.var (ABT.v' s)
 forall' :: Var v => [Text] -> Type v -> Type v
 forall' vs body = foldr forall body (map ABT.v' vs)
 
+foralls :: Var v => [v] -> Type v -> Type v
+foralls vs body = foldr forall body vs
+
+arrows :: Var v => [Type v] -> Type v -> Type v
+arrows ts result = foldr arrow result ts
+
 effect :: Ord v => [Type v] -> Type v -> Type v
 effect es t = ABT.tm (Effect es t)