{-# LANGUAGE DataKinds #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE Safe #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} module Data.Connection.Class ( castL, castR, Connection (..), ) where import safe Data.Connection.Cast import safe Data.Connection.Fixed import safe Data.Connection.Float import safe Data.Connection.Int import safe Data.Connection.Ratio import safe Data.Connection.Time import safe Data.Connection.Word import safe Data.Int import safe Data.Word import safe Numeric.Natural castL :: Connection 'L a b => Cast 'L a b castL = cast @'L castR :: Connection 'R a b => Cast 'R a b castR = cast @'R -- | A < https://ncatlab.org/nlab/show/adjoint+string chain > of Galois connections of length 2 or 3. class Connection (k :: Side) a b where cast :: Cast k a b --------------------------------------------------------------------- -- Instances --------------------------------------------------------------------- instance Connection k a a where cast = identity instance Connection k Ordering Bool where cast = bndbin instance Connection k Word8 Bool where cast = bndbin instance Connection k Word16 Bool where cast = bndbin instance Connection k Word32 Bool where cast = bndbin instance Connection k Word64 Bool where cast = bndbin instance Connection k Word Bool where cast = bndbin instance Connection k Int8 Bool where cast = bndbin instance Connection k Int16 Bool where cast = bndbin instance Connection k Int32 Bool where cast = bndbin instance Connection k Int64 Bool where cast = bndbin instance Connection k Int Bool where cast = bndbin instance Connection 'L Int8 Word8 where cast = i08w08 instance Connection 'L Word8 Word16 where cast = w08w16 instance Connection 'L Int8 Word16 where cast = i08w16 instance Connection 'L Int16 Word16 where cast = i16w16 instance Connection 'L Word8 Word32 where cast = w08w32 instance Connection 'L Word16 Word32 where cast = w16w32 instance Connection 'L Int8 Word32 where cast = i08w32 instance Connection 'L Int16 Word32 where cast = i16w32 instance Connection 'L Int32 Word32 where cast = i32w32 instance Connection 'L Word8 Word64 where cast = w08w64 instance Connection 'L Word16 Word64 where cast = w16w64 instance Connection 'L Word32 Word64 where cast = w32w64 instance Connection k Word Word64 where cast = wxxw64 instance Connection 'L Int8 Word64 where cast = i08w64 instance Connection 'L Int16 Word64 where cast = i16w64 instance Connection 'L Int32 Word64 where cast = i32w64 instance Connection 'L Int64 Word64 where cast = i64w64 instance Connection 'L Int Word64 where cast = ixxw64 instance Connection 'L Word8 Word where cast = w08wxx instance Connection 'L Word16 Word where cast = w16wxx instance Connection 'L Word32 Word where cast = w32wxx instance Connection k Word64 Word where cast = w64wxx instance Connection 'L Int8 Word where cast = i08wxx instance Connection 'L Int16 Word where cast = i16wxx instance Connection 'L Int32 Word where cast = i32wxx instance Connection 'L Int64 Word where cast = i64wxx instance Connection 'L Int Word where cast = ixxwxx instance Connection 'L Word8 Natural where cast = w08nat instance Connection 'L Word16 Natural where cast = w16nat instance Connection 'L Word32 Natural where cast = w32nat instance Connection 'L Word64 Natural where cast = w64nat instance Connection 'L Word Natural where cast = wxxnat instance Connection 'L Int8 Natural where cast = i08nat instance Connection 'L Int16 Natural where cast = i16nat instance Connection 'L Int32 Natural where cast = i32nat instance Connection 'L Int64 Natural where cast = i64nat instance Connection 'L Int Natural where cast = ixxnat instance Connection 'L Integer Natural where cast = intnat instance Connection k Uni Integer where cast = f00int instance Connection k Deci Uni where cast = f01f00 instance Connection k Centi Uni where cast = f02f00 instance Connection k Milli Uni where cast = f03f00 instance Connection k Micro Uni where cast = f06f00 instance Connection k Nano Uni where cast = f09f00 instance Connection k Pico Uni where cast = f12f00 instance Connection k Centi Deci where cast = f02f01 instance Connection k Milli Deci where cast = f03f01 instance Connection k Micro Deci where cast = f06f01 instance Connection k Nano Deci where cast = f09f01 instance Connection k Pico Deci where cast = f12f01 instance Connection k Milli Centi where cast = f03f02 instance Connection k Micro Centi where cast = f06f02 instance Connection k Nano Centi where cast = f09f02 instance Connection k Pico Centi where cast = f12f02 instance Connection k Micro Milli where cast = f06f03 instance Connection k Nano Milli where cast = f09f03 instance Connection k Pico Milli where cast = f12f03 instance Connection k Nano Micro where cast = f09f06 instance Connection k Pico Micro where cast = f12f06 instance Connection k Pico Nano where cast = f12f09 instance Connection k Double Float where cast = f64f32 instance Connection k Rational Float where cast = ratf32 instance Connection k Rational Double where cast = ratf64 instance Connection k (Extended Word8) Int16 where cast = w08i16 instance Connection k (Extended Int8) Int16 where cast = i08i16 instance Connection k (Extended Word8) Int32 where cast = w08i32 instance Connection k (Extended Word16) Int32 where cast = w16i32 instance Connection k (Extended Int8) Int32 where cast = i08i32 instance Connection k (Extended Int16) Int32 where cast = i16i32 instance Connection k (Extended Word8) Int64 where cast = w08i64 instance Connection k (Extended Word16) Int64 where cast = w16i64 instance Connection k (Extended Word32) Int64 where cast = w32i64 instance Connection k (Extended Int8) Int64 where cast = i08i64 instance Connection k (Extended Int16) Int64 where cast = i16i64 instance Connection k (Extended Int32) Int64 where cast = i32i64 instance Connection k Int Int64 where cast = ixxi64 instance Connection k (Extended Word8) Int where cast = w08ixx instance Connection k (Extended Word16) Int where cast = w16ixx instance Connection k (Extended Word32) Int where cast = w32ixx instance Connection k (Extended Int8) Int where cast = i08ixx instance Connection k (Extended Int16) Int where cast = i16ixx instance Connection k (Extended Int32) Int where cast = i32ixx instance Connection k Int64 Int where cast = i64ixx instance Connection k SystemTime Int where cast = sysixx instance Connection 'L (Extended Word8) (Maybe Integer) where cast = w08int instance Connection 'L (Extended Word16) (Maybe Integer) where cast = w16int instance Connection 'L (Extended Word32) (Maybe Integer) where cast = w32int instance Connection 'L (Extended Word64) (Maybe Integer) where cast = w64int instance Connection 'L (Extended Word) (Maybe Integer) where cast = wxxint instance Connection 'L (Extended Int8) (Maybe Integer) where cast = i08int instance Connection 'L (Extended Int16) (Maybe Integer) where cast = i16int instance Connection 'L (Extended Int32) (Maybe Integer) where cast = i32int instance Connection 'L (Extended Int64) (Maybe Integer) where cast = i64int instance Connection 'L (Extended Int) (Maybe Integer) where cast = ixxint instance Connection k Rational (Extended Word8) where cast = ratw08 instance Connection k Rational (Extended Word16) where cast = ratw16 instance Connection k Rational (Extended Word32) where cast = ratw32 instance Connection k Rational (Extended Word64) where cast = ratw64 instance Connection k Rational (Extended Word) where cast = ratwxx instance Connection k Rational (Extended Natural) where cast = ratnat instance Connection k Rational (Extended Int8) where cast = rati08 instance Connection k Rational (Extended Int16) where cast = rati16 instance Connection k Rational (Extended Int32) where cast = rati32 instance Connection k Rational (Extended Int64) where cast = rati64 instance Connection k Rational (Extended Int) where cast = ratixx instance Connection k Rational (Extended Integer) where cast = ratint instance Connection k Rational (Extended SystemTime) where cast = ratsys instance HasResolution res => Connection k Rational (Extended (Fixed res)) where cast = ratfix instance Connection k Float (Extended Word8) where cast = f32w08 instance Connection k Float (Extended Word16) where cast = f32w16 instance Connection 'L Float (Extended Word32) where cast = f32w32 instance Connection 'L Float (Extended Word64) where cast = f32w64 instance Connection 'L Float (Extended Word) where cast = f32wxx instance Connection 'L Float (Extended Natural) where cast = f32nat instance Connection k Float (Extended Int8) where cast = f32i08 instance Connection k Float (Extended Int16) where cast = f32i16 instance Connection 'L Float (Extended Int32) where cast = f32i32 instance Connection 'L Float (Extended Int64) where cast = f32i64 instance Connection 'L Float (Extended Int) where cast = f32ixx instance Connection 'L Float (Extended Integer) where cast = f32int instance Connection 'L Float (Extended SystemTime) where cast = f32sys instance HasResolution res => Connection 'L Float (Extended (Fixed res)) where cast = f32fix instance Connection k Double (Extended Word8) where cast = f64w08 instance Connection k Double (Extended Word16) where cast = f64w16 instance Connection k Double (Extended Word32) where cast = f64w32 instance Connection 'L Double (Extended Word64) where cast = f64w64 instance Connection 'L Double (Extended Word) where cast = f64wxx instance Connection 'L Double (Extended Natural) where cast = f64nat instance Connection k Double (Extended Int8) where cast = f64i08 instance Connection k Double (Extended Int16) where cast = f64i16 instance Connection k Double (Extended Int32) where cast = f64i32 instance Connection 'L Double (Extended Int64) where cast = f64i64 instance Connection 'L Double (Extended Int) where cast = f64ixx instance Connection 'L Double (Extended Integer) where cast = f64int instance Connection 'L Double (Extended SystemTime) where cast = f64sys instance HasResolution res => Connection 'L Double (Extended (Fixed res)) where cast = f64fix