Safe Haskell | Safe |
---|---|
Language | Haskell98 |
Performing size inference on a program in Combinator Normal Form
- data Type v
- data K v
- type Env v = [Scope v]
- data Scope v
- data Scheme v = Scheme {}
- generate :: Ord a => Program s a -> Maybe (Env a, Scheme a)
- lookupV :: Eq v => Env v -> v -> Maybe (Type v)
- iter :: (Eq a, Eq s) => Program s a -> Env a -> CName s a -> Maybe (Type a)
- parents :: (Eq a, Eq s) => Program s a -> Env a -> CName s a -> CName s a -> Maybe (CName s a, CName s a)
- trans :: (Eq a, Eq s) => Program s a -> CName s a -> Maybe (CName s a)
Documentation
tau ::=
Given some variable type, append a number of primes onto it. We want to be able to distinguish between the raw variable types and unification, existential Klock (rate) variables. We generate constraints so that raw variables will appear on the left of equalities, and Ks may appear on the right.
Gamma ::= ...
sigma ::= forall k... exists k... (x : t)... -> (x : t)... Note that these are all raw variable types. There is no point mentioning unification variables in this solved form.
lookupV :: Eq v => Env v -> v -> Maybe (Type v) Source #
Search for first (should be only) mention of k in environment, along with its index
iter :: (Eq a, Eq s) => Program s a -> Env a -> CName s a -> Maybe (Type a) Source #
Find iteration size of given combinator