Commit 7026edc3 authored by Oleg Grenrus's avatar Oleg Grenrus Committed by Ben Gamari
Browse files

Add 'type family (m :: Symbol) <> (n :: Symbol)'

Reviewers: dfeuer, austin, bgamari, hvr

Subscribers: dfeuer, mpickering, RyanGlScott, ekmett, yav, lelf,
simonpj, thomie

Differential Revision: https://phabricator.haskell.org/D2632

GHC Trac Issues: #12162
parent 5ff812c1
......@@ -1769,6 +1769,9 @@ callStackTyConKey = mkPreludeTyConUnique 183
typeRepTyConKey :: Unique
typeRepTyConKey = mkPreludeTyConUnique 184
typeSymbolAppendFamNameKey :: Unique
typeSymbolAppendFamNameKey = mkPreludeTyConUnique 185
---------------- Template Haskell -------------------
-- THNames.hs: USES TyConUniques 200-299
-----------------------------------------------------
......
......@@ -12,6 +12,7 @@ module TcTypeNats
, typeNatSubTyCon
, typeNatCmpTyCon
, typeSymbolCmpTyCon
, typeSymbolAppendTyCon
) where
import Type
......@@ -33,10 +34,14 @@ import PrelNames ( gHC_TYPELITS
, typeNatSubTyFamNameKey
, typeNatCmpTyFamNameKey
, typeSymbolCmpTyFamNameKey
, typeSymbolAppendFamNameKey
)
import FastString ( FastString
, fsLit, nilFS, nullFS, unpackFS, mkFastString, appendFS
)
import FastString ( FastString, fsLit )
import qualified Data.Map as Map
import Data.Maybe ( isJust )
import Data.List ( isPrefixOf, isSuffixOf )
{-------------------------------------------------------------------------------
Built-in type constructors for functions on type-level nats
......@@ -51,6 +56,7 @@ typeNatTyCons =
, typeNatSubTyCon
, typeNatCmpTyCon
, typeSymbolCmpTyCon
, typeSymbolAppendTyCon
]
typeNatAddTyCon :: TyCon
......@@ -154,6 +160,16 @@ typeSymbolCmpTyCon =
, sfInteractInert = \_ _ _ _ -> []
}
typeSymbolAppendTyCon :: TyCon
typeSymbolAppendTyCon = mkTypeSymbolFunTyCon2 name
BuiltInSynFamily
{ sfMatchFam = matchFamAppendSymbol
, sfInteractTop = interactTopAppendSymbol
, sfInteractInert = interactInertAppendSymbol
}
where
name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "AppendSymbol")
typeSymbolAppendFamNameKey typeSymbolAppendTyCon
......@@ -169,6 +185,16 @@ mkTypeNatFunTyCon2 op tcb =
Nothing
NotInjective
-- Make a binary built-in constructor of kind: Symbol -> Symbol -> Symbol
mkTypeSymbolFunTyCon2 :: Name -> BuiltInSynFamily -> TyCon
mkTypeSymbolFunTyCon2 op tcb =
mkFamilyTyCon op
(mkTemplateAnonTyConBinders [ typeSymbolKind, typeSymbolKind ])
typeSymbolKind
Nothing
(BuiltInSynFamTyCon tcb)
Nothing
NotInjective
{-------------------------------------------------------------------------------
......@@ -183,6 +209,7 @@ axAddDef
, axLeqDef
, axCmpNatDef
, axCmpSymbolDef
, axAppendSymbolDef
, axAdd0L
, axAdd0R
, axMul0L
......@@ -198,6 +225,8 @@ axAddDef
, axLeq0L
, axSubDef
, axSub0R
, axAppendSymbol0R
, axAppendSymbol0L
:: CoAxiomRule
axAddDef = mkBinAxiom "AddDef" typeNatAddTyCon $
......@@ -222,10 +251,23 @@ axCmpSymbolDef =
, coaxrRole = Nominal
, coaxrProves = \cs ->
do [Pair s1 s2, Pair t1 t2] <- return cs
[s2', t2'] <- traverse isStrLitTy [s2, t2]
s2' <- isStrLitTy s2
t2' <- isStrLitTy t2
return (mkTyConApp typeSymbolCmpTyCon [s1,t1] ===
ordering (compare s2' t2')) }
axAppendSymbolDef = CoAxiomRule
{ coaxrName = fsLit "AppendSymbolDef"
, coaxrAsmpRoles = [Nominal, Nominal]
, coaxrRole = Nominal
, coaxrProves = \cs ->
do [Pair s1 s2, Pair t1 t2] <- return cs
s2' <- isStrLitTy s2
t2' <- isStrLitTy t2
let z = mkStrLitTy (appendFS s2' t2')
return (mkTyConApp typeSymbolAppendTyCon [s1, t1] === z)
}
axSubDef = mkBinAxiom "SubDef" typeNatSubTyCon $
\x y -> fmap num (minus x y)
......@@ -245,6 +287,10 @@ axCmpNatRefl = mkAxiom1 "CmpNatRefl"
axCmpSymbolRefl = mkAxiom1 "CmpSymbolRefl"
$ \(Pair s _) -> (cmpSymbol s s) === ordering EQ
axLeq0L = mkAxiom1 "Leq0L" $ \(Pair s _) -> (num 0 <== s) === bool True
axAppendSymbol0R = mkAxiom1 "Concat0R"
$ \(Pair s t) -> (mkStrLitTy nilFS `appendSymbol` s) === t
axAppendSymbol0L = mkAxiom1 "Concat0L"
$ \(Pair s t) -> (s `appendSymbol` mkStrLitTy nilFS) === t
typeNatCoAxiomRules :: Map.Map FastString CoAxiomRule
typeNatCoAxiomRules = Map.fromList $ map (\x -> (coaxrName x, x))
......@@ -254,6 +300,7 @@ typeNatCoAxiomRules = Map.fromList $ map (\x -> (coaxrName x, x))
, axLeqDef
, axCmpNatDef
, axCmpSymbolDef
, axAppendSymbolDef
, axAdd0L
, axAdd0R
, axMul0L
......@@ -268,6 +315,8 @@ typeNatCoAxiomRules = Map.fromList $ map (\x -> (coaxrName x, x))
, axCmpSymbolRefl
, axLeq0L
, axSubDef
, axAppendSymbol0R
, axAppendSymbol0L
]
......@@ -297,6 +346,9 @@ cmpNat s t = mkTyConApp typeNatCmpTyCon [s,t]
cmpSymbol :: Type -> Type -> Type
cmpSymbol s t = mkTyConApp typeSymbolCmpTyCon [s,t]
appendSymbol :: Type -> Type -> Type
appendSymbol s t = mkTyConApp typeSymbolAppendTyCon [s, t]
(===) :: Type -> Type -> Pair Type
x === y = Pair x y
......@@ -352,8 +404,9 @@ mkBinAxiom str tc f =
, coaxrRole = Nominal
, coaxrProves = \cs ->
do [Pair s1 s2, Pair t1 t2] <- return cs
[s2', t2'] <- traverse isNumLitTy [s2, t2]
z <- f s2' t2'
s2' <- isNumLitTy s2
t2' <- isNumLitTy t2
z <- f s2' t2'
return (mkTyConApp tc [s1,t1] === z)
}
......@@ -444,6 +497,16 @@ matchFamCmpSymbol [s,t]
mbY = isStrLitTy t
matchFamCmpSymbol _ = Nothing
matchFamAppendSymbol :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamAppendSymbol [s,t]
| Just x <- mbX, nullFS x = Just (axAppendSymbol0R, [t], t)
| Just y <- mbY, nullFS y = Just (axAppendSymbol0L, [s], s)
| Just x <- mbX, Just y <- mbY =
Just (axAppendSymbolDef, [s,t], mkStrLitTy (appendFS x y))
where
mbX = isStrLitTy s
mbY = isStrLitTy t
matchFamAppendSymbol _ = Nothing
{-------------------------------------------------------------------------------
Interact with axioms
......@@ -542,8 +605,26 @@ interactTopCmpSymbol [s,t] r
| Just EQ <- isOrderingLitTy r = [ s === t ]
interactTopCmpSymbol _ _ = []
interactTopAppendSymbol :: [Xi] -> Xi -> [Pair Type]
interactTopAppendSymbol [s,t] r
-- (AppendSymbol a b ~ "") => (a ~ "", b ~ "")
| Just z <- mbZ, nullFS z =
[s === mkStrLitTy nilFS, t === mkStrLitTy nilFS ]
-- (AppendSymbol "foo" b ~ "foobar") => (b ~ "bar")
| Just x <- fmap unpackFS mbX, Just z <- fmap unpackFS mbZ, x `isPrefixOf` z =
[ t === mkStrLitTy (mkFastString $ drop (length x) z) ]
-- (AppendSymbol f "bar" ~ "foobar") => (f ~ "foo")
| Just y <- fmap unpackFS mbY, Just z <- fmap unpackFS mbZ, y `isSuffixOf` z =
[ t === mkStrLitTy (mkFastString $ take (length z - length y) z) ]
where
mbX = isStrLitTy s
mbY = isStrLitTy t
mbZ = isStrLitTy r
interactTopAppendSymbol _ _ = []
{-------------------------------------------------------------------------------
Interaction with inerts
......@@ -592,9 +673,12 @@ interactInertLeq [x1,y1] z1 [x2,y2] z2
interactInertLeq _ _ _ _ = []
interactInertAppendSymbol :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
interactInertAppendSymbol [x1,y1] z1 [x2,y2] z2
| sameZ && tcEqType x1 x2 = [ y1 === y2 ]
| sameZ && tcEqType y1 y2 = [ x1 === x2 ]
where sameZ = tcEqType z1 z2
interactInertAppendSymbol _ _ _ _ = []
......
......@@ -226,6 +226,9 @@ See ``changelog.md`` in the ``base`` package for full release notes.
provided in GHC's version of the ``Read`` class, and allows users to write
more efficient ``Read1`` and ``Read2`` instances.
- Add ``type family AppendSymbol (m :: Symbol) (n :: Symbol) :: Symbol`` to
``GHC.TypeLits``
binary
~~~~~~
......
......@@ -35,6 +35,7 @@ module GHC.TypeLits
-- * Functions on type literals
, type (<=), type (<=?), type (+), type (*), type (^), type (-)
, AppendSymbol
, CmpNat, CmpSymbol
-- * User-defined type errors
......@@ -203,6 +204,10 @@ type family (m :: Nat) ^ (n :: Nat) :: Nat
-- @since 4.7.0.0
type family (m :: Nat) - (n :: Nat) :: Nat
-- | Concatenation of type-level symbols.
--
-- @since 4.10.0.0
type family AppendSymbol (m ::Symbol) (n :: Symbol) :: Symbol
-- | A description of a custom type error.
data {-kind-} ErrorMessage = Text Symbol
......
......@@ -40,6 +40,9 @@
* Add `plusForeignPtr` to `Foreign.ForeignPtr`.
* Add `type family AppendSymbol (m :: Symbol) (n :: Symbol) :: Symbol` to `GHC.TypeLits`
(#12162)
## 4.9.0.0 *May 2016*
* Bundled with GHC 8.0
......
......@@ -12,6 +12,9 @@ type (GHC.TypeLits.<=) (x :: GHC.Types.Nat) (y :: GHC.Types.Nat) =
type family (GHC.TypeLits.<=?) (a :: GHC.Types.Nat)
(b :: GHC.Types.Nat)
:: Bool
type family GHC.TypeLits.AppendSymbol (a :: GHC.Types.Symbol)
(b :: GHC.Types.Symbol)
:: GHC.Types.Symbol
type family GHC.TypeLits.CmpNat (a :: GHC.Types.Nat)
(b :: GHC.Types.Nat)
:: Ordering
......
{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies #-}
module TcTypeNatSimple where
import GHC.TypeLits
import Data.Proxy
--------------------------------------------------------------------------------
-- Test evaluation
te1 :: Proxy (AppendSymbol "" x) -> Proxy x
te1 = id
te2 :: Proxy (AppendSymbol x "") -> Proxy x
te2 = id
te3 :: Proxy (AppendSymbol "type" "level") -> Proxy "typelevel"
te3 = id
--------------------------------------------------------------------------------
-- Test interactions with inerts
tei1 :: Proxy (AppendSymbol y x) -> Proxy x -> ()
tei1 _ _ = ()
tei2 :: Proxy (AppendSymbol "foo" x) -> ()
tei2 _ = ()
tei3 :: Proxy (AppendSymbol x "foo") -> ()
tei3 _ = ()
......@@ -427,6 +427,7 @@ test('T7888', normal, compile, [''])
test('T7891', normal, compile, [''])
test('T7903', normal, compile, [''])
test('TcTypeNatSimple', normal, compile, [''])
test('TcTypeSymbolSimple', normal, compile, [''])
test('TcCoercibleCompile', [], compile, [''])
test('T8392', normal, compile, [''])
test('T8474', normal, compile, [''])
......
......@@ -9,9 +9,15 @@ import Data.Proxy
tsub :: Proxy (x + y) -> Proxy y -> Proxy x
tsub _ _ = Proxy
tsub2 :: Proxy (x + y) -> (Proxy x, Proxy y)
tsub2 _ = (Proxy, Proxy)
tdiv :: Proxy (x * y) -> Proxy y -> Proxy x
tdiv _ _ = Proxy
tdiv2 :: Proxy (x * y) -> (Proxy x, Proxy y)
tdiv2 _ = (Proxy, Proxy)
troot :: Proxy (x ^ y) -> Proxy y -> Proxy x
troot _ _ = Proxy
......@@ -23,12 +29,14 @@ tleq _ = Proxy
main :: IO ()
main = print [ sh (tsub (Proxy :: Proxy 5) (Proxy :: Proxy 3)) == "2"
, let (p, q) = tsub2 (Proxy :: Proxy 0)
in (sh p, sh q) == ("0", "0")
, sh (tdiv (Proxy :: Proxy 8) (Proxy :: Proxy 2)) == "4"
, let (p, q) = tdiv2 (Proxy :: Proxy 1)
in (sh p, sh q) == ("1", "1")
, sh (troot (Proxy :: Proxy 9) (Proxy :: Proxy 2)) == "3"
, sh (tlog (Proxy :: Proxy 8) (Proxy :: Proxy 2)) == "3"
, sh (tleq (Proxy :: Proxy 0)) == "0"
]
where
sh x = show (natVal x)
[True,True,True,True,True]
[True,True,True,True,True,True,True]
{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies #-}
module Main(main) where
import GHC.TypeLits
import Data.Proxy
--------------------------------------------------------------------------------
-- Test top-reactions
tappend :: Proxy (AppendSymbol x y) -> Proxy x -> Proxy y
tappend _ _ = Proxy
tappend2 :: Proxy (AppendSymbol x y) -> (Proxy x, Proxy y)
tappend2 _ = (Proxy, Proxy)
main :: IO ()
main = print [ symbolVal (tappend (Proxy :: Proxy "abc") (Proxy :: Proxy "ab"))
== "c"
, let (p, q) = tappend2 (Proxy :: Proxy "")
in (symbolVal p, symbolVal q) == ("", "")
]
where
sh x = show (natVal x)
......@@ -102,6 +102,7 @@ test('T5913', normal, compile_and_run, [''])
test('T7748', normal, compile_and_run, [''])
test('T7861', [omit_ways('debug'), exit_code(1)], compile_and_run, [''])
test('TcTypeNatSimpleRun', normal, compile_and_run, [''])
test('TcTypeSymbolSimpleRun', normal, compile_and_run, [''])
test('T8119', normal, ghci_script, ['T8119.script'])
test('T8492', normal, compile_and_run, [''])
test('T8739', normal, compile_and_run, [''])
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment