Skip to content
Snippets Groups Projects
Select Git revision
  • b1dcbc9edd964b9d0cab6c26db4d502840011ac4
  • main default protected
  • 75389691-a67c-422a-91e9-aa58bfb5-main-patch-32205
  • test-pipe
  • extended-scripts
  • structured-badges
  • guix-pipeline
  • cabal-pipeline
8 results

Types.hs

Blame
  • KindLinter.hs 2.12 KiB
    {-# 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.HList
    import           Data.Kind       (Type)
    import           Data.Map.Strict
    import           Data.Void       (Void)
    import           GHC.TypeLits    (KnownSymbol, Symbol, symbolVal)
    
    
    func :: a -> HList [Int, String]
    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 .*.
      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?