summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGaborGreif <>2017-10-12 12:52:00 (GMT)
committerhdiff <hdiff@hdiff.luite.com>2017-10-12 12:52:00 (GMT)
commita4745ac352f85f50e476a920dec7097e66abeb65 (patch)
tree6b5ef68f94c8c760b5bbeb00e1675c21d75f99a9
parent17d73f2fd0e812abf8bc31d2e10da2415fee90d6 (diff)
version 0.1.10.1.1
-rw-r--r--Main.hs18
-rw-r--r--TyFamWitnesses.hs5
-rw-r--r--changelog.md12
-rw-r--r--tyfam-witnesses.cabal5
4 files changed, 34 insertions, 6 deletions
diff --git a/Main.hs b/Main.hs
index faef0ea..3ad0c19 100644
--- a/Main.hs
+++ b/Main.hs
@@ -1,6 +1,7 @@
{-# LANGUAGE ScopedTypeVariables, TemplateHaskell, StandaloneDeriving, TypeFamilies, GADTs
, ViewPatterns, TypeOperators, TypeApplications, StandaloneDeriving
- , UnicodeSyntax, PatternSynonyms, FlexibleContexts, DataKinds, UndecidableInstances #-}
+ , UnicodeSyntax, PatternSynonyms, FlexibleContexts, DataKinds, UndecidableInstances
+ , TypeFamilyDependencies #-}
-- invoke as: ghci Main.hs -ddump-parsed -ddump-rn
-- or in GHCi: :set -ddump-parsed -ddump-rn
@@ -63,7 +64,16 @@ witnesses [d| data Peano = Z | S Peano
|]
-deriving instance Show (FromPeanoRefl n)
+deriving instance Show (ToPeanoRefl n)
+deriving instance Show (FromPeanoRefl p)
+
+witnesses [d| type family Unspell (w :: Symbol) = (r :: Nat) | r -> w where
+ Unspell "zero" = 0
+ Unspell "one" = 1
+ Unspell "two" = 2
+ Unspell "three" = 3
+ |]
+deriving instance Show (UnspellRefl w)
main = runQ (witnesses stuffhave2) >>= print
@@ -116,3 +126,7 @@ t0@Nothing = lemma "joe" (typeOf ord) (typeOf "joe")
Just u0 = reify_FromPeano (typeRep @Z)
Just u1 = reify_FromPeano (typeRep @(S Z))
Just u2 = reify_FromPeano (typeRep @(S (S Z)))
+
+Just un0 = reify_Unspell (typeRep @"zero")
+Just un1 = reify_Unspell (typeRep @"one")
+Just un2 = reify_Unspell (typeRep @"two")
diff --git a/TyFamWitnesses.hs b/TyFamWitnesses.hs
index fbce1d5..af7498a 100644
--- a/TyFamWitnesses.hs
+++ b/TyFamWitnesses.hs
@@ -12,6 +12,7 @@
-- see https://ghc.haskell.org/t/14296
-- - clients need to activate ScopedTypeVariables
-- - type family a /=/ b where, how to name the artifacts?
+-- - take advantage of 'InjectivityAnn'?
module TyFamWitnesses (witnesses, stuffhave, stuffhave1, stuffhave2, pattern Lifted, pattern Fun') where
import GHC.Exts
@@ -76,7 +77,7 @@ witnesses decsQ =
pure $ decs ++ datas ++ concat funcs
buildGADT :: Dec -> Q (Maybe (Dec, (Name, [Exp], Dec)))
-buildGADT fam@(ClosedTypeFamilyD (TypeFamilyHead name tyvars _ Nothing) clauses) =
+buildGADT fam@(ClosedTypeFamilyD (TypeFamilyHead name tyvars _ _) clauses) =
do ns <- sequence constrNames
n <- newName (occ ++ "Refl")
pure (pure (DataD [] n tyvars Nothing (constrs ns n) [], (n, ConE <$> ns, fam)))
@@ -96,7 +97,7 @@ instance Lift Exp where lift = pure
pattern TRACE <- ((`traceShow` ()) -> ())
buildReifier :: (Name, [Exp], Dec) -> DecsQ
-buildReifier (dname, constrs, ClosedTypeFamilyD (TypeFamilyHead name formals _ Nothing) clauses) =
+buildReifier (dname, constrs, ClosedTypeFamilyD (TypeFamilyHead name formals _ _) clauses) =
do n <- newName ("reify_" ++ occ)
tyr <- [t|TypeRep|]
mbe <- [t|Maybe|]
diff --git a/changelog.md b/changelog.md
new file mode 100644
index 0000000..c299eba
--- /dev/null
+++ b/changelog.md
@@ -0,0 +1,12 @@
+Version History
+############
+
+_newest first_
+
+`0.1.1` Bugfix, *injective* type families now allowed (2017-10-12)
+
+`0.1` Bugfixes (2017-10-12)
+
+`0.0.0.1` Documentation fixes (2017-10-08)
+
+`0.0` Initial release (2017-10-08)
diff --git a/tyfam-witnesses.cabal b/tyfam-witnesses.cabal
index a555c53..2bfb2af 100644
--- a/tyfam-witnesses.cabal
+++ b/tyfam-witnesses.cabal
@@ -1,7 +1,7 @@
name: tyfam-witnesses
-version: 0.1
+version: 0.1.1
synopsis: Provide proof witnesses for closed type family evaluation
-description: Template Haskell routine for generating from type family 'Foo'
+description: Template Haskell routine for generating from type family $Foo$
.
[@FooRefl@]: a GADT capturing the equalities of each type family clause
[@reify_Foo@]: a function that analyses 'TypeRep's and reifies the matching clause as a 'FooRefl'
@@ -16,6 +16,7 @@ category: Development
stability: experimental
build-type: Simple
+extra-source-files: changelog.md
cabal-version: >=1.10
tested-with: GHC == 8.2.1