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

add TH support for nested higher kinded types #2515

Open
wants to merge 3 commits into
base: main
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
102 changes: 85 additions & 17 deletions dhall/src/Dhall/TH.hs
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,7 @@ import Language.Haskell.TH.Syntax (DerivClause (..), DerivStrategy (..))

import qualified Data.List as List
import qualified Data.Map as Map
import qualified Data.Maybe as Maybe
import qualified Data.Set as Set
import qualified Data.Text as Text
import qualified Data.Time as Time
Expand Down Expand Up @@ -132,8 +133,6 @@ toNestedHaskellType
-> Q Type
toNestedHaskellType typeParams haskellTypes = loop
where
predicate dhallType haskellType = Core.judgmentallyEqual (code haskellType) dhallType

document dhallType =
mconcat
[ "Unsupported nested type\n"
Expand Down Expand Up @@ -207,17 +206,91 @@ toNestedHaskellType typeParams haskellTypes = loop

Var v
| Just (V param index) <- List.find (v ==) typeParams -> do
let name = Syntax.mkName $ (Text.unpack param) ++ (show index)

return (VarT name)
return $ VarT $ Syntax.mkName $ (Text.unpack param) ++ (show index)

| otherwise -> fail $ message v

_ | Just haskellType <- List.find (predicate dhallType) haskellTypes -> do
let name = Syntax.mkName (Text.unpack (typeName haskellType))
_ -> do
res <- mapM (judgementallyEqualNested dhallType) haskellTypes

maybe (fail $ message dhallType) return $ Maybe.listToMaybe $ Maybe.catMaybes res

haskellTypeToConT haskellType = ConT $ Syntax.mkName (Text.unpack (typeName haskellType))

judgementallyEqualNested dhallType haskellType = case partitionTypeVars (code haskellType) of
([], haskellType')
| Core.judgmentallyEqual haskellType' dhallType ->
return $ Just $ haskellTypeToConT haskellType

| otherwise -> return Nothing

(params, bareHaskellType)
| Just nested <- gatherNestedVars Map.empty bareHaskellType dhallType -> do
let con = haskellTypeToConT haskellType

nestedTypes <- mapM (toNestedHaskellType typeParams haskellTypes)
$ Maybe.mapMaybe (`Map.lookup` nested) params

return $ Just $ foldr (flip AppT) con $ reverse nestedTypes

| otherwise -> return Nothing

gatherNestedVars nested haskellType dhallType = case (haskellType, dhallType) of

-- if haskellType has a typevar, store whatever the dhallType has unless
-- this typevar already has an existing dhalltype which doesn't match
((Var v), newDhallType) -> case Map.lookup v nested of
Just oldDhallType
| Core.judgmentallyEqual oldDhallType newDhallType -> Just nested

| otherwise -> Nothing

Nothing -> Just $ Map.insert v newDhallType nested

return (ConT name)
| otherwise -> fail $ message dhallType
-- iterate through all records one level down
(Record m1, Record m2)
| Dhall.Map.keysSet m1 == Dhall.Map.keysSet m2
-> gatherNestedVarsAcross (Just nested)
$ Dhall.Map.elems
$ Dhall.Map.intersectionWith combineRec m1 m2

| otherwise -> Nothing

-- ditto for unions, except here we need to check if each alternate
-- has either no type or a matching type
(Union m1, Union m2)
| Dhall.Map.keysSet m1 == Dhall.Map.keysSet m2 -> do
es <- sequence $ Dhall.Map.elems $ Dhall.Map.intersectionWith combineUnion m1 m2
gatherNestedVarsAcross (Just nested) $ Maybe.catMaybes es

| otherwise -> Nothing

-- otherwise there is nothing to store and no further levels into which
-- to drill futher, so compare directly
(i, j)
| Core.judgmentallyEqual i j -> Just nested

| otherwise -> Nothing

gatherNestedVarsAcross nested [] = nested
gatherNestedVarsAcross Nothing _ = Nothing
gatherNestedVarsAcross (Just nested) ((ht, dt):rest) =
gatherNestedVarsAcross (gatherNestedVars nested ht dt) rest

combineRec x y = (Core.recordFieldValue x, Core.recordFieldValue y)

combineUnion (Just x) (Just y) = Just (Just (x, y)) -- two alts with types (valid)
combineUnion Nothing Nothing = Just Nothing -- two alts with no types (valid)
combineUnion _ _ = Nothing -- anything else (invalid)


-- | Split expression into type variables (from leading lambdas if present) and
-- its nested expression.
partitionTypeVars :: Expr s a -> ([Var], Expr s a)
partitionTypeVars = first (reverse . numberConsecutive) . go []
where
go acc (Lam _ (FunctionBinding _ v _ _ _) rest) = go (v:acc) rest
go acc rest = (acc, rest)

-- | A deriving clause for `Generic`.
derivingGenericClause :: DerivClause
Expand Down Expand Up @@ -252,14 +325,9 @@ toDeclaration
-> Q [Dec]
toDeclaration generateOptions@GenerateOptions{..} haskellTypes typ =
case typ of
SingleConstructor{..} -> uncurry (fromSingle typeName constructorName) $ getTypeParams code
MultipleConstructors{..} -> uncurry (fromMulti typeName) $ getTypeParams code
SingleConstructor{..} -> uncurry (fromSingle typeName constructorName) $ partitionTypeVars code
MultipleConstructors{..} -> uncurry (fromMulti typeName) $ partitionTypeVars code
where
getTypeParams = first numberConsecutive . getTypeParams_ []

getTypeParams_ acc (Lam _ (FunctionBinding _ v _ _ _) rest) = getTypeParams_ (v:acc) rest
getTypeParams_ acc rest = (acc, rest)

derivingClauses = [ derivingGenericClause | generateFromDhallInstance || generateToDhallInstance ]

interpretOptions = generateToInterpretOptions generateOptions typ
Expand Down Expand Up @@ -337,7 +405,7 @@ toDeclaration generateOptions@GenerateOptions{..} haskellTypes typ =

-- | Number each variable, starting at 0
numberConsecutive :: [Text.Text] -> [Var]
numberConsecutive = snd . List.mapAccumR go Map.empty . reverse
numberConsecutive = reverse . snd . List.mapAccumR go Map.empty . reverse
where
go m k =
let (i, m') = Map.updateLookupWithKey (\_ j -> Just $ j + 1) k m
Expand Down
28 changes: 28 additions & 0 deletions dhall/tests/Dhall/Test/TH.hs
Original file line number Diff line number Diff line change
Expand Up @@ -116,10 +116,16 @@ Dhall.TH.makeHaskellTypesWith (Dhall.TH.defaultGenerateOptions
})
[ SingleConstructor "MyHKSingle" "HKSingle" "./tests/th/HigherKindSingle.dhall"
, MultipleConstructors "MyHKUnion" "./tests/th/HigherKindUnion.dhall"
, SingleConstructor "MyHKInnerS" "HKInnerS" "(./tests/th/HigherKindNested.dhall).InnerS"
, MultipleConstructors "MyHKInnerU" "(./tests/th/HigherKindNested.dhall).InnerU"
, SingleConstructor "MyHKOuter" "HKOuter" "(./tests/th/HigherKindNested.dhall).Outer"
]

type MyHKSingle_ = MyHKSingle Maybe Int
type MyHKUnion_ = MyHKUnion Bool Int
type MyHKInnerS_ = MyHKInnerS Bool Data.Text.Text
type MyHKInnerU_ = MyHKInnerU Int Data.Text.Text
type MyHKOuter_ = MyHKOuter Bool Int

deriving instance Eq MyHKSingle_
deriving instance Show MyHKSingle_
Expand All @@ -133,6 +139,24 @@ deriving instance Dhall.Generic MyHKUnion_
instance Dhall.FromDhall MyHKUnion_
instance Dhall.ToDhall MyHKUnion_

deriving instance Eq MyHKInnerS_
deriving instance Show MyHKInnerS_
deriving instance Dhall.Generic MyHKInnerS_
instance Dhall.FromDhall MyHKInnerS_
instance Dhall.ToDhall MyHKInnerS_

deriving instance Eq MyHKInnerU_
deriving instance Show MyHKInnerU_
deriving instance Dhall.Generic MyHKInnerU_
instance Dhall.FromDhall MyHKInnerU_
instance Dhall.ToDhall MyHKInnerU_

deriving instance Eq MyHKOuter_
deriving instance Show MyHKOuter_
deriving instance Dhall.Generic MyHKOuter_
instance Dhall.FromDhall MyHKOuter_
instance Dhall.ToDhall MyHKOuter_

testMakeHaskellTypesWith :: TestTree
testMakeHaskellTypesWith = Tasty.HUnit.testCase "makeHaskellTypesWith" $ do
let text0 = "let T = ./tests/th/example.dhall in T.A { x = True, y = [] : List Text }"
Expand Down Expand Up @@ -167,6 +191,10 @@ testMakeHaskellTypesWith = Tasty.HUnit.testCase "makeHaskellTypesWith" $ do
refHKUnion1 = MyBar 1 :: MyHKUnion_
myTest textHKUnion1 refHKUnion1

let textHKOuter = "let T = (./tests/th/HigherKindNested.dhall) in T.Outer Bool Int { oFoo = { iFoo = True, iBar = \"\" }, oBar = T.InnerU.Ifoo +1 }"
refHKOuter = MyHKOuter { myObar = MyIfoo 1, myOfoo = (MyHKInnerS { myIbar = "", myIfoo = True }) } :: MyHKOuter_
myTest textHKOuter refHKOuter

where
myTest text ref = do
expr <- Dhall.inputExpr text
Expand Down
10 changes: 10 additions & 0 deletions dhall/tests/th/HigherKindNested.dhall
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
let InnerS = \(x : Type) -> \(y : Type) -> { ifoo : x, ibar : y }

let InnerU = \(x : Type) -> \(y : Type) -> < Ifoo : x | Ibar : y >

let Outer =
\(i : Type) ->
\(j : Type) ->
{ ofoo : InnerS i Text, obar : InnerU j Text }

in { InnerS, InnerU, Outer }
Loading