hakaru-0.7.0: A probabilistic programming language
CopyrightCopyright (c) 2017 the Hakaru team
LicenseBSD3
Stabilityexperimental
PortabilityGHC-only
Safe HaskellNone
LanguageHaskell2010

Language.Hakaru.Syntax.TypeCheck.Unification

Description

Ad-hoc implementation of unification (ad-hoc because polytypes are inexpressible, and this module makes no attempt to express them).

Documentation

type Metadata = Maybe SourceSpan Source #

type Unify1 (t :: Hakaru -> Hakaru) r x = Sing x -> Metadata -> (forall a. x ~ t a => Sing a -> TypeCheckMonad r) -> TypeCheckMonad r Source #

type Unify2 (t :: Hakaru -> Hakaru -> Hakaru) r x = Sing x -> Metadata -> (forall a b. x ~ t a b => Sing a -> Sing b -> TypeCheckMonad r) -> TypeCheckMonad r Source #

class TCMTypeRepr x where Source #

Methods

toTypeRepr :: x -> Maybe (Either Text (Some1 (Sing :: Hakaru -> *))) Source #

Instances

Instances details
TCMTypeRepr () Source # 
Instance details

Defined in Language.Hakaru.Syntax.TypeCheck.Unification

Methods

toTypeRepr :: () -> Maybe (Either Text (Some1 Sing)) Source #

TCMTypeRepr Text Source # 
Instance details

Defined in Language.Hakaru.Syntax.TypeCheck.Unification

Methods

toTypeRepr :: Text -> Maybe (Either Text (Some1 Sing)) Source #

TCMTypeRepr (Sing x) Source # 
Instance details

Defined in Language.Hakaru.Syntax.TypeCheck.Unification

Methods

toTypeRepr :: Sing x -> Maybe (Either Text (Some1 Sing)) Source #

unifyMeasure :: Unify1 'HMeasure r x Source #

unifyArray :: Unify1 'HArray r x Source #

unifyFun :: Unify2 '(:->) r x Source #

unifyPair :: Unify2 HPair r x Source #

matchTypes :: (TCMTypeRepr t0, TCMTypeRepr t1) => Sing (x :: Hakaru) -> Sing y -> Metadata -> t0 -> t1 -> (x ~ y => TypeCheckMonad r) -> TypeCheckMonad r Source #