vinyl-0.4.1: Extensible Records

Safe HaskellNone




class xs <: ys where Source

One record is a subtype of another if the fields of the latter are a subset of the fields of the former.


cast :: Rec el f xs -> Rec el f ys Source


(<:) k xs ([] k) 
((∈) k y xs, (<:) k xs ys) => (<:) k xs ((:) k y ys) 

type (:~:) r1 r2 = (r1 <: r2, r2 <: r1) Source

If two records types are subtypes of each other, that means that they differ only in order of fields.

(~=) :: (Eq (Rec el f xs), xs :~: ys) => Rec el f xs -> Rec el f ys -> Bool Source

Term-level record congruence.

type family RecAll el f rs c :: Constraint Source


type RecAll k k1 el f ([] k) c = () 
type RecAll k * el f ((:) k r rs) c = (c (f (($) * k el r)), RecAll k * el f rs c)