Language.Hakaru.Syntax.SArgs

Documentation

type SArgsSing = SArgs (Pointwise (Lift1 ()) Sing)

data SArgs :: ([Hakaru] -> Hakaru -> *) -> [([Hakaru], Hakaru)] -> * where

The arguments to a (:$) node in the Term; that is, a list of ASTs, where the whole list is indexed by a (type-level) list of the indices of each element.

Constructors

End :: SArgs abt '[]

(:*) :: !(abt vars a) -> !(SArgs abt args) -> SArgs abt ('(vars, a) ': args) infixr 5

Instances

Traversable21 SArgs

Methods

traverse21 :: Applicative f => (forall (h :: k1) (i :: k2). a h i -> f (b h i)) -> SArgs a j -> f (SArgs b j)

Foldable21 SArgs

Methods

fold21 :: Monoid m => SArgs (Lift2 m) j -> m

foldMap21 :: Monoid m => (forall (h :: k1) (i :: k2). a h i -> m) -> SArgs a j -> m

Functor21 SArgs

Methods

fmap21 :: (forall (h :: k1) (i :: k2). a h i -> b h i) -> SArgs a j -> SArgs b j

JmEq2 abt => JmEq1 (SArgs abt :: [([Hakaru], Hakaru)] -> *)

Methods

jmEq1 :: SArgs abt i -> SArgs abt j -> Maybe (TypeEq i j)

Eq2 abt => Eq1 (SArgs abt :: [([Hakaru], Hakaru)] -> *)

Methods

eq1 :: SArgs abt i -> SArgs abt i -> Bool

Show2 abt => Show1 (SArgs abt :: [([Hakaru], Hakaru)] -> *)

Methods

showsPrec1 :: Int -> SArgs abt i -> ShowS

show1 :: SArgs abt i -> String

Eq2 abt => Eq (SArgs abt args)

Methods

(==) :: SArgs abt args -> SArgs abt args -> Bool

(/=) :: SArgs abt args -> SArgs abt args -> Bool

Show2 abt => Show (SArgs abt args)

Methods

showsPrec :: Int -> SArgs abt args -> ShowS

show :: SArgs abt args -> String

showList :: [SArgs abt args] -> ShowS

type LC (a :: Hakaru) = '('[], a)

Locally closed values (i.e., not binding forms) of a given type. TODO: come up with a better name

getSArgsSing :: forall abt xs m. Applicative m => (forall ys a. abt ys a -> m (Sing a)) -> SArgs abt xs -> m (SArgsSing xs)