From 1530a4646b5bb7ab2930d1433eda87d5f0936125 Mon Sep 17 00:00:00 2001 From: stuebinm Date: Sat, 15 Jan 2022 00:46:30 +0100 Subject: use hpack and clean up modules as annoying as yaml is, cabal's package format is somehow worse, apparently --- lib/KindLinter.hs | 64 +++++++++++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 55 insertions(+), 9 deletions(-) (limited to 'lib/KindLinter.hs') diff --git a/lib/KindLinter.hs b/lib/KindLinter.hs index 4ecf067..ccca1db 100644 --- a/lib/KindLinter.hs +++ b/lib/KindLinter.hs @@ -1,14 +1,23 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE PartialTypeSignatures #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} module KindLinter where -import Data.Map.Strict -import Data.HList -import GHC.TypeLits (Symbol, KnownSymbol) +import Data.HList +import Data.Kind (Type) +import Data.Map.Strict +import Data.Void (Void) +import GHC.TypeLits (KnownSymbol, Symbol, symbolVal) func :: a -> HList [Int, String] @@ -17,12 +26,49 @@ func _ = hBuild 10 "test" field :: forall a. KnownSymbol a => Label a field = Label +data Linter a = Some a | None +type LintSingleton b a = Tagged b a + +-- newtype LintSet a :: Record '[LintSingleton Int] +-- newtype LintSet (a :: Type -> Record '[Type]) = Record (a Void) + +type SomeList (a :: Type) = Record '[Tagged "test" a] + +type family MkList (b :: [Symbol]) a where + MkList '[] _ = '[] + MkList (x:xs) a = Tagged x a : MkList xs a + +type Lints labels a = Record (MkList labels a) + +type KnownProperties = '["hello", "test"] + +record :: Lints KnownProperties Int record = + Label @"hello" .=. 20 .*. Label @"test" .=. 10 .*. - field @"x" .=. 20 .*. + -- field @"x" .=. 20 .*. emptyRecord + +class KnownList a where + listVal :: Proxy a -> [String] + +instance KnownList '[] where + listVal _ = [] + +instance (KnownList xs, KnownSymbol x) => KnownList (x:xs) where + listVal _ = symbolVal (Proxy @x) : listVal (Proxy @xs) + + +lints :: [String] +lints = listVal (Proxy @KnownProperties) + +-- TODO: how to pattern match on that? +doSth :: forall a b ctxt. (KnownList a, b ~ MkList a (Linter ctxt)) => Proxy b -> String -> Linter ctxt +doSth _ name = None -- want to get a different result for each value of name in a + -- is there a better way than using listVal / something related to it? + -- TODO: these should be limited to Tagged "symbol" (LintWriter a) tileLints = field @"test" .=. (\a -> a) .*. -- cgit v1.2.3