-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | An implementation of the Levenberg-Marquardt algorithm -- -- The Levenberg-Marquardt algorithm is an iterative technique that finds -- a local minimum of a function that is expressed as the sum of squares -- of nonlinear functions. It has become a standard technique for -- nonlinear least-squares problems and can be thought of as a -- combination of steepest descent and the Gauss-Newton method. When the -- current solution is far from the correct one, the algorithm behaves -- like a steepest descent method: slow, but guaranteed to converge. When -- the current solution is close to the correct solution, it becomes a -- Gauss-Newton method. -- -- Optional box- and linear constraints can be given. Both single and -- double precision floating point types are supported. -- -- The actual algorithm is implemented in a C library which is bundled -- with bindings-levmar which this package depends on. See: -- http://www.ics.forth.gr/~lourakis/levmar/. -- -- This library consists of two layers: -- --
-- *TypeLevelNat> witnessNat :: S (S (S Z)) -- S (S (S Z)) --witnessNat :: (Nat n) => n -- | A value-level natural indexed with an equivalent type-level natural. data N n Zero :: N Z Succ :: N n -> N (S n) nat :: (Nat n) => n -> N n instance (Show n) => Show (S n) instance Show Z instance (Nat p) => Nat (S p) instance Nat Z module SizedList -- | A list which is indexed with a type-level natural that denotes the -- size of the list. data SizedList n a Nil :: SizedList Z a (:::) :: a -> SizedList n a -> SizedList (S n) a -- | Fold a binary operator over a SizedList. foldr :: (a -> b -> b) -> b -> SizedList n a -> b -- | Fold a binary operator yielding a value with a natural number indexed -- type over a SizedList. foldrN :: (forall m. a -> b m -> b (S m)) -> b Z -> SizedList n a -> b n -- | Convert a SizedList to a normal list. toList :: SizedList n a -> [a] -- | Returns the length of the SizedList. length :: SizedList n a -> N n -- | Convert a normal list to a SizedList. If the length of the -- given list does not equal n, Nothing is returned. fromList :: (Nat n) => [a] -> Maybe (SizedList n a) -- | Convert a normal list to a SizeList. If the length of the -- given list does not equal n, an error is thrown. unsafeFromList :: (Nat n) => [a] -> SizedList n a -- | replicate x :: SizedList n a returns a SizedList of -- n xs. replicate :: (Nat n) => a -> SizedList n a instance (Show a) => Show (SizedList n a) instance Functor (SizedList n) module NFunction -- | A NFunction n a b is a function which takes n -- arguments of type a and returns a b. For example: -- NFunction (S (S (S Z))) a b ~ (a -> a -> a -> b) -- | f $* xs applies the n-arity function f to -- each of the arguments in the n-sized list xs. ($*) :: NFunction n a b -> SizedList n a -> b class (Nat n) => ComposeN n compose :: (ComposeN n) => n -> a -> (b -> c) -> NFunction n a b -> NFunction n a c instance (ComposeN n) => ComposeN (S n) instance ComposeN Z -- | For additional documentation see the documentation of the levmar C -- library which this library is based on: -- http://www.ics.forth.gr/~lourakis/levmar/ module LevMar.Intermediate -- | A functional relation describing measurements represented as a -- function from a list of parameters to a list of expected measurements. -- --
-- hatfldc :: Model Double -- hatfldc [p0, p1, p2, p3] = [ p0 - 1.0 -- , p0 - sqrt p1 -- , p1 - sqrt p2 -- , p3 - 1.0 -- ] --type Model r = [r] -> [r] -- | The jacobian of the Model function. Expressed as a function -- from a list of parameters to a list of lists which for each expected -- measurement describes the partial derivatives of the parameters. -- -- See: -- http://en.wikipedia.org/wiki/Jacobian_matrix_and_determinant -- --
-- hatfldc_jac :: Jacobian Double -- hatfldc_jac _ p1 p2 _ = [ [1.0, 0.0, 0.0, 0.0] -- , [1.0, -0.5 / sqrt p1, 0.0, 0.0] -- , [0.0, 1.0, -0.5 / sqrt p2, 0.0] -- , [0.0, 0.0, 0.0, 1.0] -- ] --type Jacobian r = [r] -> [[r]] -- | The Levenberg-Marquardt algorithm is overloaded to work on -- Double and Float. class LevMarable r levmar :: (LevMarable r) => Model r -> Maybe (Jacobian r) -> [r] -> [r] -> Integer -> Options r -> Maybe [r] -> Maybe [r] -> Maybe (LinearConstraints r) -> Maybe [r] -> Either LevMarError ([r], Info r, CovarMatrix r) -- | Linear constraints consisting of a constraints matrix, kxm and -- a right hand constraints vector, kx1 where m is the -- number of parameters and k is the number of constraints. type LinearConstraints r = ([[r]], [r]) -- | Minimization options data Options r Opts :: r -> r -> r -> r -> r -> Options r -- | Scale factor for initial mu. optScaleInitMu :: Options r -> r -- | Stopping thresholds for ||J^T e||_inf. optStopNormInfJacTe :: Options r -> r -- | Stopping thresholds for ||Dp||_2. optStopNorm2Dp :: Options r -> r -- | Stopping thresholds for ||e||_2. optStopNorm2E :: Options r -> r -- | Step used in the difference approximation to the Jacobian. If -- optDelta<0, the Jacobian is approximated with central -- differences which are more accurate (but slower!) compared to the -- forward differences employed by default. optDelta :: Options r -> r -- | Default minimization options defaultOpts :: (Fractional r) => Options r -- | Information regarding the minimization. data Info r Info :: r -> r -> r -> r -> r -> Integer -> StopReason -> Integer -> Integer -> Integer -> Info r -- | ||e||_2 at initial parameters. infNorm2initE :: Info r -> r -- | ||e||_2 at estimated parameters. infNorm2E :: Info r -> r -- | ||J^T e||_inf at estimated parameters. infNormInfJacTe :: Info r -> r -- | ||Dp||_2 at estimated parameters. infNorm2Dp :: Info r -> r -- | mu/max[J^T J]_ii ] at estimated parameters. infMuDivMax :: Info r -> r -- | Number of iterations. infNumIter :: Info r -> Integer -- | Reason for terminating. infStopReason :: Info r -> StopReason -- | Number of function evaluations. infNumFuncEvals :: Info r -> Integer -- | Number of jacobian evaluations. infNumJacobEvals :: Info r -> Integer -- | Number of linear systems solved, i.e. attempts for reducing error. infNumLinSysSolved :: Info r -> Integer -- | Reason for terminating. data StopReason -- | Stopped because of small gradient J^T e. SmallGradient :: StopReason -- | Stopped because of small Dp. SmallDp :: StopReason -- | Stopped because maximum iterations was reached. MaxIterations :: StopReason -- | Stopped because of singular matrix. Restart from current estimated -- parameters with increased optScaleInitMu. SingularMatrix :: StopReason -- | Stopped because no further error reduction is possible. Restart with -- increased optScaleInitMu. SmallestError :: StopReason -- | Stopped because of small ||e||_2. SmallNorm2E :: StopReason -- | Stopped because model function returned invalid values (i.e. NaN or -- Inf). This is a user error. InvalidValues :: StopReason -- | Covariance matrix corresponding to LS solution. type CovarMatrix r = [[r]] data LevMarError -- | Generic error (not one of the others) LevMarError :: LevMarError -- | A call to a lapack subroutine failed in the underlying C levmar -- library. LapackError :: LevMarError -- | At least one lower bound exceeds the upper one. FailedBoxCheck :: LevMarError -- | A call to malloc failed in the underlying C levmar library. MemoryAllocationFailure :: LevMarError -- | The matrix of constraints cannot have more rows than columns. ConstraintMatrixRowsGtCols :: LevMarError -- | Constraints matrix is not of full row rank. ConstraintMatrixNotFullRowRank :: LevMarError -- | Cannot solve a problem with fewer measurements than unknowns. In case -- linear constraints are provided, this error is also returned when the -- number of measurements is smaller than the number of unknowns minus -- the number of equality constraints. TooFewMeasurements :: LevMarError instance Show LevMarError instance Show StopReason instance Enum StopReason instance (Show r) => Show (Info r) instance (Show r) => Show (Options r) instance LevMarable Double instance LevMarable Float -- | A levmar variant that uses Automatic Differentiation to automatically -- compute the Jacobian. -- -- For additional documentation see the documentation of the levmar C -- library which this library is based on: -- http://www.ics.forth.gr/~lourakis/levmar/ module LevMar.Intermediate.AD -- | A functional relation describing measurements represented as a -- function from a list of parameters to a list of expected measurements. -- --
-- hatfldc :: Model Double -- hatfldc [p0, p1, p2, p3] = [ p0 - 1.0 -- , p0 - sqrt p1 -- , p1 - sqrt p2 -- , p3 - 1.0 -- ] --type Model r = [r] -> [r] -- | The jacobian of the Model function. Expressed as a function -- from a list of parameters to a list of lists which for each expected -- measurement describes the partial derivatives of the parameters. -- -- See: -- http://en.wikipedia.org/wiki/Jacobian_matrix_and_determinant -- --
-- hatfldc_jac :: Jacobian Double -- hatfldc_jac _ p1 p2 _ = [ [1.0, 0.0, 0.0, 0.0] -- , [1.0, -0.5 / sqrt p1, 0.0, 0.0] -- , [0.0, 1.0, -0.5 / sqrt p2, 0.0] -- , [0.0, 0.0, 0.0, 1.0] -- ] --type Jacobian r = [r] -> [[r]] -- | Compute the Jacobian of the Model using Automatic -- Differentiation. jacobianOf :: (HasBasis r, (Basis r) ~ (), VectorSpace (Scalar r)) => Model (r :~> r) -> Jacobian r -- | The Levenberg-Marquardt algorithm is overloaded to work on -- Double and Float. class LevMarable r -- | The Levenberg-Marquardt algorithm that automatically computes the -- Jacobian using automatic differentiation of the model function. -- -- Warning: Don't apply levmar to Models that apply -- methods of the Eq and Ord classes to the parameters. -- These methods are undefined for ':~>'!!! levmar :: (HasBasis r, (Basis r) ~ (), VectorSpace (Scalar r), LevMarable r) => Model (r :~> r) -> [r] -> [r] -> Integer -> Options r -> Maybe [r] -> Maybe [r] -> Maybe (LinearConstraints r) -> Maybe [r] -> Either LevMarError ([r], Info r, CovarMatrix r) -- | Linear constraints consisting of a constraints matrix, kxm and -- a right hand constraints vector, kx1 where m is the -- number of parameters and k is the number of constraints. type LinearConstraints r = ([[r]], [r]) -- | Minimization options data Options r Opts :: r -> r -> r -> r -> r -> Options r -- | Scale factor for initial mu. optScaleInitMu :: Options r -> r -- | Stopping thresholds for ||J^T e||_inf. optStopNormInfJacTe :: Options r -> r -- | Stopping thresholds for ||Dp||_2. optStopNorm2Dp :: Options r -> r -- | Stopping thresholds for ||e||_2. optStopNorm2E :: Options r -> r -- | Step used in the difference approximation to the Jacobian. If -- optDelta<0, the Jacobian is approximated with central -- differences which are more accurate (but slower!) compared to the -- forward differences employed by default. optDelta :: Options r -> r -- | Default minimization options defaultOpts :: (Fractional r) => Options r -- | Information regarding the minimization. data Info r Info :: r -> r -> r -> r -> r -> Integer -> StopReason -> Integer -> Integer -> Integer -> Info r -- | ||e||_2 at initial parameters. infNorm2initE :: Info r -> r -- | ||e||_2 at estimated parameters. infNorm2E :: Info r -> r -- | ||J^T e||_inf at estimated parameters. infNormInfJacTe :: Info r -> r -- | ||Dp||_2 at estimated parameters. infNorm2Dp :: Info r -> r -- | mu/max[J^T J]_ii ] at estimated parameters. infMuDivMax :: Info r -> r -- | Number of iterations. infNumIter :: Info r -> Integer -- | Reason for terminating. infStopReason :: Info r -> StopReason -- | Number of function evaluations. infNumFuncEvals :: Info r -> Integer -- | Number of jacobian evaluations. infNumJacobEvals :: Info r -> Integer -- | Number of linear systems solved, i.e. attempts for reducing error. infNumLinSysSolved :: Info r -> Integer -- | Reason for terminating. data StopReason -- | Stopped because of small gradient J^T e. SmallGradient :: StopReason -- | Stopped because of small Dp. SmallDp :: StopReason -- | Stopped because maximum iterations was reached. MaxIterations :: StopReason -- | Stopped because of singular matrix. Restart from current estimated -- parameters with increased optScaleInitMu. SingularMatrix :: StopReason -- | Stopped because no further error reduction is possible. Restart with -- increased optScaleInitMu. SmallestError :: StopReason -- | Stopped because of small ||e||_2. SmallNorm2E :: StopReason -- | Stopped because model function returned invalid values (i.e. NaN or -- Inf). This is a user error. InvalidValues :: StopReason -- | Covariance matrix corresponding to LS solution. type CovarMatrix r = [[r]] data LevMarError -- | Generic error (not one of the others) LevMarError :: LevMarError -- | A call to a lapack subroutine failed in the underlying C levmar -- library. LapackError :: LevMarError -- | At least one lower bound exceeds the upper one. FailedBoxCheck :: LevMarError -- | A call to malloc failed in the underlying C levmar library. MemoryAllocationFailure :: LevMarError -- | The matrix of constraints cannot have more rows than columns. ConstraintMatrixRowsGtCols :: LevMarError -- | Constraints matrix is not of full row rank. ConstraintMatrixNotFullRowRank :: LevMarError -- | Cannot solve a problem with fewer measurements than unknowns. In case -- linear constraints are provided, this error is also returned when the -- number of measurements is smaller than the number of unknowns minus -- the number of equality constraints. TooFewMeasurements :: LevMarError -- | This module provides the Levenberg-Marquardt algorithm specialised for -- curve-fitting. -- -- For additional documentation see the documentation of the levmar C -- library which this library is based on: -- http://www.ics.forth.gr/~lourakis/levmar/ module LevMar.Intermediate.Fitting -- | A functional relation describing measurements represented as a -- function from a list of parameters and an x-value to an expected -- measurement. -- --
-- quad :: Num r => Model r r -- quad [a, b, c] x = a*x^2 + b*x + c --type Model r a = [r] -> a -> r -- | This type synonym expresses that usually the a in -- Model r a equals the type of the parameters. type SimpleModel r = Model r r -- | The jacobian of the Model function. Expressed as a function -- from a list of parameters and an x-value to the partial derivatives of -- the parameters. -- -- See: -- http://en.wikipedia.org/wiki/Jacobian_matrix_and_determinant -- --
-- quadJacob :: Num r => Jacobian N3 r r -- quadJacob [_, _, _] x = [ x^2 -- with respect to a -- , x -- with respect to b -- , 1 -- with respect to c -- ] ---- -- Notice you don't have to differentiate for x. type Jacobian r a = [r] -> a -> [r] -- | This type synonym expresses that usually the a in -- Jacobian r a equals the type of the parameters. type SimpleJacobian r = Jacobian r r -- | The Levenberg-Marquardt algorithm is overloaded to work on -- Double and Float. class LevMarable r -- | The Levenberg-Marquardt algorithm specialised for curve-fitting. levmar :: (LevMarable r) => Model r a -> Maybe (Jacobian r a) -> [r] -> [(a, r)] -> Integer -> Options r -> Maybe [r] -> Maybe [r] -> Maybe (LinearConstraints r) -> Maybe [r] -> Either LevMarError ([r], Info r, CovarMatrix r) -- | Linear constraints consisting of a constraints matrix, kxm and -- a right hand constraints vector, kx1 where m is the -- number of parameters and k is the number of constraints. type LinearConstraints r = ([[r]], [r]) -- | Minimization options data Options r Opts :: r -> r -> r -> r -> r -> Options r -- | Scale factor for initial mu. optScaleInitMu :: Options r -> r -- | Stopping thresholds for ||J^T e||_inf. optStopNormInfJacTe :: Options r -> r -- | Stopping thresholds for ||Dp||_2. optStopNorm2Dp :: Options r -> r -- | Stopping thresholds for ||e||_2. optStopNorm2E :: Options r -> r -- | Step used in the difference approximation to the Jacobian. If -- optDelta<0, the Jacobian is approximated with central -- differences which are more accurate (but slower!) compared to the -- forward differences employed by default. optDelta :: Options r -> r -- | Default minimization options defaultOpts :: (Fractional r) => Options r -- | Information regarding the minimization. data Info r Info :: r -> r -> r -> r -> r -> Integer -> StopReason -> Integer -> Integer -> Integer -> Info r -- | ||e||_2 at initial parameters. infNorm2initE :: Info r -> r -- | ||e||_2 at estimated parameters. infNorm2E :: Info r -> r -- | ||J^T e||_inf at estimated parameters. infNormInfJacTe :: Info r -> r -- | ||Dp||_2 at estimated parameters. infNorm2Dp :: Info r -> r -- | mu/max[J^T J]_ii ] at estimated parameters. infMuDivMax :: Info r -> r -- | Number of iterations. infNumIter :: Info r -> Integer -- | Reason for terminating. infStopReason :: Info r -> StopReason -- | Number of function evaluations. infNumFuncEvals :: Info r -> Integer -- | Number of jacobian evaluations. infNumJacobEvals :: Info r -> Integer -- | Number of linear systems solved, i.e. attempts for reducing error. infNumLinSysSolved :: Info r -> Integer -- | Reason for terminating. data StopReason -- | Stopped because of small gradient J^T e. SmallGradient :: StopReason -- | Stopped because of small Dp. SmallDp :: StopReason -- | Stopped because maximum iterations was reached. MaxIterations :: StopReason -- | Stopped because of singular matrix. Restart from current estimated -- parameters with increased optScaleInitMu. SingularMatrix :: StopReason -- | Stopped because no further error reduction is possible. Restart with -- increased optScaleInitMu. SmallestError :: StopReason -- | Stopped because of small ||e||_2. SmallNorm2E :: StopReason -- | Stopped because model function returned invalid values (i.e. NaN or -- Inf). This is a user error. InvalidValues :: StopReason -- | Covariance matrix corresponding to LS solution. type CovarMatrix r = [[r]] data LevMarError -- | Generic error (not one of the others) LevMarError :: LevMarError -- | A call to a lapack subroutine failed in the underlying C levmar -- library. LapackError :: LevMarError -- | At least one lower bound exceeds the upper one. FailedBoxCheck :: LevMarError -- | A call to malloc failed in the underlying C levmar library. MemoryAllocationFailure :: LevMarError -- | The matrix of constraints cannot have more rows than columns. ConstraintMatrixRowsGtCols :: LevMarError -- | Constraints matrix is not of full row rank. ConstraintMatrixNotFullRowRank :: LevMarError -- | Cannot solve a problem with fewer measurements than unknowns. In case -- linear constraints are provided, this error is also returned when the -- number of measurements is smaller than the number of unknowns minus -- the number of equality constraints. TooFewMeasurements :: LevMarError -- | A levmar variant specialised for curve-fitting that uses Automatic -- Differentiation to automatically compute the Jacobian. -- -- For additional documentation see the documentation of the levmar C -- library which this library is based on: -- http://www.ics.forth.gr/~lourakis/levmar/ module LevMar.Intermediate.Fitting.AD -- | A functional relation describing measurements represented as a -- function from a list of parameters and an x-value to an expected -- measurement. -- --
-- quad :: Num r => Model r r -- quad [a, b, c] x = a*x^2 + b*x + c --type Model r a = [r] -> a -> r -- | This type synonym expresses that usually the a in -- Model r a equals the type of the parameters. type SimpleModel r = Model r r -- | The jacobian of the Model function. Expressed as a function -- from a list of parameters and an x-value to the partial derivatives of -- the parameters. -- -- See: -- http://en.wikipedia.org/wiki/Jacobian_matrix_and_determinant -- --
-- quadJacob :: Num r => Jacobian N3 r r -- quadJacob [_, _, _] x = [ x^2 -- with respect to a -- , x -- with respect to b -- , 1 -- with respect to c -- ] ---- -- Notice you don't have to differentiate for x. type Jacobian r a = [r] -> a -> [r] -- | This type synonym expresses that usually the a in -- Jacobian r a equals the type of the parameters. type SimpleJacobian r = Jacobian r r -- | Compute the Jacobian of the Model using Automatic -- Differentiation. jacobianOf :: (HasBasis r, (Basis r) ~ (), VectorSpace (Scalar r)) => Model (r :~> r) a -> Jacobian r a -- | The Levenberg-Marquardt algorithm is overloaded to work on -- Double and Float. class LevMarable r -- | The Levenberg-Marquardt algorithm specialised for curve-fitting that -- automatically computes the Jacobian using automatic differentiation of -- the model function. -- -- Warning: Don't apply levmar to Models that apply -- methods of the Eq and Ord classes to the parameters. -- These methods are undefined for ':~>'!!! levmar :: (HasBasis r, (Basis r) ~ (), VectorSpace (Scalar r), LevMarable r) => Model (r :~> r) a -> [r] -> [(a, r)] -> Integer -> Options r -> Maybe [r] -> Maybe [r] -> Maybe (LinearConstraints r) -> Maybe [r] -> Either LevMarError ([r], Info r, CovarMatrix r) -- | Linear constraints consisting of a constraints matrix, kxm and -- a right hand constraints vector, kx1 where m is the -- number of parameters and k is the number of constraints. type LinearConstraints r = ([[r]], [r]) -- | Minimization options data Options r Opts :: r -> r -> r -> r -> r -> Options r -- | Scale factor for initial mu. optScaleInitMu :: Options r -> r -- | Stopping thresholds for ||J^T e||_inf. optStopNormInfJacTe :: Options r -> r -- | Stopping thresholds for ||Dp||_2. optStopNorm2Dp :: Options r -> r -- | Stopping thresholds for ||e||_2. optStopNorm2E :: Options r -> r -- | Step used in the difference approximation to the Jacobian. If -- optDelta<0, the Jacobian is approximated with central -- differences which are more accurate (but slower!) compared to the -- forward differences employed by default. optDelta :: Options r -> r -- | Default minimization options defaultOpts :: (Fractional r) => Options r -- | Information regarding the minimization. data Info r Info :: r -> r -> r -> r -> r -> Integer -> StopReason -> Integer -> Integer -> Integer -> Info r -- | ||e||_2 at initial parameters. infNorm2initE :: Info r -> r -- | ||e||_2 at estimated parameters. infNorm2E :: Info r -> r -- | ||J^T e||_inf at estimated parameters. infNormInfJacTe :: Info r -> r -- | ||Dp||_2 at estimated parameters. infNorm2Dp :: Info r -> r -- | mu/max[J^T J]_ii ] at estimated parameters. infMuDivMax :: Info r -> r -- | Number of iterations. infNumIter :: Info r -> Integer -- | Reason for terminating. infStopReason :: Info r -> StopReason -- | Number of function evaluations. infNumFuncEvals :: Info r -> Integer -- | Number of jacobian evaluations. infNumJacobEvals :: Info r -> Integer -- | Number of linear systems solved, i.e. attempts for reducing error. infNumLinSysSolved :: Info r -> Integer -- | Reason for terminating. data StopReason -- | Stopped because of small gradient J^T e. SmallGradient :: StopReason -- | Stopped because of small Dp. SmallDp :: StopReason -- | Stopped because maximum iterations was reached. MaxIterations :: StopReason -- | Stopped because of singular matrix. Restart from current estimated -- parameters with increased optScaleInitMu. SingularMatrix :: StopReason -- | Stopped because no further error reduction is possible. Restart with -- increased optScaleInitMu. SmallestError :: StopReason -- | Stopped because of small ||e||_2. SmallNorm2E :: StopReason -- | Stopped because model function returned invalid values (i.e. NaN or -- Inf). This is a user error. InvalidValues :: StopReason -- | Covariance matrix corresponding to LS solution. type CovarMatrix r = [[r]] data LevMarError -- | Generic error (not one of the others) LevMarError :: LevMarError -- | A call to a lapack subroutine failed in the underlying C levmar -- library. LapackError :: LevMarError -- | At least one lower bound exceeds the upper one. FailedBoxCheck :: LevMarError -- | A call to malloc failed in the underlying C levmar library. MemoryAllocationFailure :: LevMarError -- | The matrix of constraints cannot have more rows than columns. ConstraintMatrixRowsGtCols :: LevMarError -- | Constraints matrix is not of full row rank. ConstraintMatrixNotFullRowRank :: LevMarError -- | Cannot solve a problem with fewer measurements than unknowns. In case -- linear constraints are provided, this error is also returned when the -- number of measurements is smaller than the number of unknowns minus -- the number of equality constraints. TooFewMeasurements :: LevMarError -- | This module provides the Levenberg-Marquardt algorithm specialised for -- curve-fitting. -- -- For additional documentation see the documentation of the levmar C -- library which this library is based on: -- http://www.ics.forth.gr/~lourakis/levmar/ module LevMar.Fitting -- | A functional relation describing measurements represented as a -- function from m parameters and an x-value to an expected -- measurement. -- -- For example, the quadratic function f(x) = a*x^2 + b*x + c -- can be written as: -- --
-- type N3 = S (S (S Z)) -- -- quad :: Num r => Model N3 r r -- quad a b c x = a*x^2 + b*x + c --type Model m r a = NFunction m r (a -> r) -- | This type synonym expresses that usually the a in -- Model m r a equals the type of the parameters. type SimpleModel m r = Model m r r -- | The jacobian of the Model function. Expressed as a function -- from n parameters and an x-value to the m partial -- derivatives of the parameters. -- -- See: -- http://en.wikipedia.org/wiki/Jacobian_matrix_and_determinant -- -- For example, the jacobian of the quadratic function f(x) = a*x^2 + -- b*x + c can be written as: -- --
-- type N3 = S (S (S Z)) -- -- quadJacob :: Num r => Jacobian N3 r r -- quadJacob _ _ _ x = x^2 -- with respect to a -- ::: x -- with respect to b -- ::: 1 -- with respect to c -- ::: Nil ---- -- Notice you don't have to differentiate for x. type Jacobian m r a = NFunction m r (a -> SizedList m r) -- | This type synonym expresses that usually the a in -- Jacobian m r a equals the type of the parameters. type SimpleJacobian m r = Jacobian m r r -- | The Levenberg-Marquardt algorithm is overloaded to work on -- Double and Float. class LevMarable r -- | The Levenberg-Marquardt algorithm specialised for curve-fitting. levmar :: (Nat m, Nat k, LevMarable r) => (Model m r a) -> Maybe (Jacobian m r a) -> SizedList m r -> [(a, r)] -> Integer -> Options r -> Maybe (SizedList m r) -> Maybe (SizedList m r) -> Maybe (LinearConstraints k m r) -> Maybe (SizedList m r) -> Either LevMarError (SizedList m r, Info r, CovarMatrix m r) -- | Linear constraints consisting of a constraints matrix, kxn and -- a right hand constraints vector, kx1 where n is the -- number of parameters and k is the number of constraints. type LinearConstraints k n r = (Matrix k n r, SizedList k r) -- | Value to denote the absense of any linear constraints over the -- parameters of the model function. Use this instead of Nothing -- because the type parameter which contains the number of constraints -- can't be inferred. noLinearConstraints :: (Nat n) => Maybe (LinearConstraints Z n r) -- | A nxm matrix is a sized list of n sized lists of length -- m. type Matrix n m r = SizedList n (SizedList m r) -- | Minimization options data Options r Opts :: r -> r -> r -> r -> r -> Options r -- | Scale factor for initial mu. optScaleInitMu :: Options r -> r -- | Stopping thresholds for ||J^T e||_inf. optStopNormInfJacTe :: Options r -> r -- | Stopping thresholds for ||Dp||_2. optStopNorm2Dp :: Options r -> r -- | Stopping thresholds for ||e||_2. optStopNorm2E :: Options r -> r -- | Step used in the difference approximation to the Jacobian. If -- optDelta<0, the Jacobian is approximated with central -- differences which are more accurate (but slower!) compared to the -- forward differences employed by default. optDelta :: Options r -> r -- | Default minimization options defaultOpts :: (Fractional r) => Options r -- | Information regarding the minimization. data Info r Info :: r -> r -> r -> r -> r -> Integer -> StopReason -> Integer -> Integer -> Integer -> Info r -- | ||e||_2 at initial parameters. infNorm2initE :: Info r -> r -- | ||e||_2 at estimated parameters. infNorm2E :: Info r -> r -- | ||J^T e||_inf at estimated parameters. infNormInfJacTe :: Info r -> r -- | ||Dp||_2 at estimated parameters. infNorm2Dp :: Info r -> r -- | mu/max[J^T J]_ii ] at estimated parameters. infMuDivMax :: Info r -> r -- | Number of iterations. infNumIter :: Info r -> Integer -- | Reason for terminating. infStopReason :: Info r -> StopReason -- | Number of function evaluations. infNumFuncEvals :: Info r -> Integer -- | Number of jacobian evaluations. infNumJacobEvals :: Info r -> Integer -- | Number of linear systems solved, i.e. attempts for reducing error. infNumLinSysSolved :: Info r -> Integer -- | Reason for terminating. data StopReason -- | Stopped because of small gradient J^T e. SmallGradient :: StopReason -- | Stopped because of small Dp. SmallDp :: StopReason -- | Stopped because maximum iterations was reached. MaxIterations :: StopReason -- | Stopped because of singular matrix. Restart from current estimated -- parameters with increased optScaleInitMu. SingularMatrix :: StopReason -- | Stopped because no further error reduction is possible. Restart with -- increased optScaleInitMu. SmallestError :: StopReason -- | Stopped because of small ||e||_2. SmallNorm2E :: StopReason -- | Stopped because model function returned invalid values (i.e. NaN or -- Inf). This is a user error. InvalidValues :: StopReason -- | Covariance matrix corresponding to LS solution. type CovarMatrix n r = Matrix n n r data LevMarError -- | Generic error (not one of the others) LevMarError :: LevMarError -- | A call to a lapack subroutine failed in the underlying C levmar -- library. LapackError :: LevMarError -- | At least one lower bound exceeds the upper one. FailedBoxCheck :: LevMarError -- | A call to malloc failed in the underlying C levmar library. MemoryAllocationFailure :: LevMarError -- | The matrix of constraints cannot have more rows than columns. ConstraintMatrixRowsGtCols :: LevMarError -- | Constraints matrix is not of full row rank. ConstraintMatrixNotFullRowRank :: LevMarError -- | Cannot solve a problem with fewer measurements than unknowns. In case -- linear constraints are provided, this error is also returned when the -- number of measurements is smaller than the number of unknowns minus -- the number of equality constraints. TooFewMeasurements :: LevMarError -- | Type-level natural denoting zero data Z -- | Type-level natural denoting the Successor of another type-level -- natural. data S n -- | Class of all type-level naturals. class Nat n -- | A list which is indexed with a type-level natural that denotes the -- size of the list. data SizedList n a Nil :: SizedList Z a (:::) :: a -> SizedList n a -> SizedList (S n) a -- | A NFunction n a b is a function which takes n -- arguments of type a and returns a b. For example: -- NFunction (S (S (S Z))) a b ~ (a -> a -> a -> b) -- | This module provides the Levenberg-Marquardt algorithm specialised for -- curve-fitting that uses Automatic Differentiation to automatically -- compute the Jacobian. -- -- For additional documentation see the documentation of the levmar C -- library which this library is based on: -- http://www.ics.forth.gr/~lourakis/levmar/ module LevMar.Fitting.AD -- | A functional relation describing measurements represented as a -- function from m parameters and an x-value to an expected -- measurement. -- -- For example, the quadratic function f(x) = a*x^2 + b*x + c -- can be written as: -- --
-- type N3 = S (S (S Z)) -- -- quad :: Num r => Model N3 r r -- quad a b c x = a*x^2 + b*x + c --type Model m r a = NFunction m r (a -> r) -- | This type synonym expresses that usually the a in -- Model m r a equals the type of the parameters. type SimpleModel m r = Model m r r -- | The Levenberg-Marquardt algorithm is overloaded to work on -- Double and Float. class LevMarable r -- | The Levenberg-Marquardt algorithm specialised for curve-fitting that -- automatically computes the Jacobian using automatic differentiation of -- the model function. -- -- Warning: Don't apply levmar to Models that apply -- methods of the Eq and Ord classes to the parameters. -- These methods are undefined for ':~>'!!! levmar :: (Nat m, Nat k, HasBasis r, (Basis r) ~ (), VectorSpace (Scalar r), LevMarable r) => Model m (r :~> r) a -> SizedList m r -> [(a, r)] -> Integer -> Options r -> Maybe (SizedList m r) -> Maybe (SizedList m r) -> Maybe (LinearConstraints k m r) -> Maybe (SizedList m r) -> Either LevMarError (SizedList m r, Info r, CovarMatrix m r) -- | Linear constraints consisting of a constraints matrix, kxn and -- a right hand constraints vector, kx1 where n is the -- number of parameters and k is the number of constraints. type LinearConstraints k n r = (Matrix k n r, SizedList k r) -- | Value to denote the absense of any linear constraints over the -- parameters of the model function. Use this instead of Nothing -- because the type parameter which contains the number of constraints -- can't be inferred. noLinearConstraints :: (Nat n) => Maybe (LinearConstraints Z n r) -- | A nxm matrix is a sized list of n sized lists of length -- m. type Matrix n m r = SizedList n (SizedList m r) -- | Minimization options data Options r Opts :: r -> r -> r -> r -> r -> Options r -- | Scale factor for initial mu. optScaleInitMu :: Options r -> r -- | Stopping thresholds for ||J^T e||_inf. optStopNormInfJacTe :: Options r -> r -- | Stopping thresholds for ||Dp||_2. optStopNorm2Dp :: Options r -> r -- | Stopping thresholds for ||e||_2. optStopNorm2E :: Options r -> r -- | Step used in the difference approximation to the Jacobian. If -- optDelta<0, the Jacobian is approximated with central -- differences which are more accurate (but slower!) compared to the -- forward differences employed by default. optDelta :: Options r -> r -- | Default minimization options defaultOpts :: (Fractional r) => Options r -- | Information regarding the minimization. data Info r Info :: r -> r -> r -> r -> r -> Integer -> StopReason -> Integer -> Integer -> Integer -> Info r -- | ||e||_2 at initial parameters. infNorm2initE :: Info r -> r -- | ||e||_2 at estimated parameters. infNorm2E :: Info r -> r -- | ||J^T e||_inf at estimated parameters. infNormInfJacTe :: Info r -> r -- | ||Dp||_2 at estimated parameters. infNorm2Dp :: Info r -> r -- | mu/max[J^T J]_ii ] at estimated parameters. infMuDivMax :: Info r -> r -- | Number of iterations. infNumIter :: Info r -> Integer -- | Reason for terminating. infStopReason :: Info r -> StopReason -- | Number of function evaluations. infNumFuncEvals :: Info r -> Integer -- | Number of jacobian evaluations. infNumJacobEvals :: Info r -> Integer -- | Number of linear systems solved, i.e. attempts for reducing error. infNumLinSysSolved :: Info r -> Integer -- | Reason for terminating. data StopReason -- | Stopped because of small gradient J^T e. SmallGradient :: StopReason -- | Stopped because of small Dp. SmallDp :: StopReason -- | Stopped because maximum iterations was reached. MaxIterations :: StopReason -- | Stopped because of singular matrix. Restart from current estimated -- parameters with increased optScaleInitMu. SingularMatrix :: StopReason -- | Stopped because no further error reduction is possible. Restart with -- increased optScaleInitMu. SmallestError :: StopReason -- | Stopped because of small ||e||_2. SmallNorm2E :: StopReason -- | Stopped because model function returned invalid values (i.e. NaN or -- Inf). This is a user error. InvalidValues :: StopReason -- | Covariance matrix corresponding to LS solution. type CovarMatrix n r = Matrix n n r data LevMarError -- | Generic error (not one of the others) LevMarError :: LevMarError -- | A call to a lapack subroutine failed in the underlying C levmar -- library. LapackError :: LevMarError -- | At least one lower bound exceeds the upper one. FailedBoxCheck :: LevMarError -- | A call to malloc failed in the underlying C levmar library. MemoryAllocationFailure :: LevMarError -- | The matrix of constraints cannot have more rows than columns. ConstraintMatrixRowsGtCols :: LevMarError -- | Constraints matrix is not of full row rank. ConstraintMatrixNotFullRowRank :: LevMarError -- | Cannot solve a problem with fewer measurements than unknowns. In case -- linear constraints are provided, this error is also returned when the -- number of measurements is smaller than the number of unknowns minus -- the number of equality constraints. TooFewMeasurements :: LevMarError -- | Type-level natural denoting zero data Z -- | Type-level natural denoting the Successor of another type-level -- natural. data S n -- | Class of all type-level naturals. class Nat n -- | A list which is indexed with a type-level natural that denotes the -- size of the list. data SizedList n a Nil :: SizedList Z a (:::) :: a -> SizedList n a -> SizedList (S n) a -- | A NFunction n a b is a function which takes n -- arguments of type a and returns a b. For example: -- NFunction (S (S (S Z))) a b ~ (a -> a -> a -> b) -- | For additional documentation see the documentation of the levmar C -- library which this library is based on: -- http://www.ics.forth.gr/~lourakis/levmar/ module LevMar -- | A functional relation describing measurements represented as a -- function from m parameters to n expected -- measurements. -- -- An example from Demo.hs: -- --
-- type N4 = S (S (S (S Z))) -- -- hatfldc :: Model N4 N4 Double -- hatfldc p0 p1 p2 p3 = p0 - 1.0 -- ::: p0 - sqrt p1 -- ::: p1 - sqrt p2 -- ::: p3 - 1.0 -- ::: Nil --type Model m n r = NFunction m r (SizedList n r) -- | The jacobian of the Model function. Expressed as a function -- from m parameters to a nxm matrix -- which for each of the n expected measurement describes the -- m partial derivatives of the parameters. -- -- See: -- http://en.wikipedia.org/wiki/Jacobian_matrix_and_determinant -- -- For example the jacobian of the above hatfldc model is: -- --
-- type N4 = S (S (S (S Z))) -- -- hatfldc_jac :: Jacobian N4 N4 Double -- hatfldc_jac _ p1 p2 _ = (1.0 ::: 0.0 ::: 0.0 ::: 0.0 ::: Nil) -- ::: (1.0 ::: -0.5 / sqrt p1 ::: 0.0 ::: 0.0 ::: Nil) -- ::: (0.0 ::: 1.0 ::: -0.5 / sqrt p2 ::: 0.0 ::: Nil) -- ::: (0.0 ::: 0.0 ::: 0.0 ::: 1.0 ::: Nil) -- ::: Nil --type Jacobian m n r = NFunction m r (Matrix n m r) -- | The Levenberg-Marquardt algorithm is overloaded to work on -- Double and Float. class LevMarable r -- | The Levenberg-Marquardt algorithm. levmar :: (Nat m, Nat n, Nat k, LevMarable r) => (Model m n r) -> Maybe (Jacobian m n r) -> SizedList m r -> SizedList n r -> Integer -> Options r -> Maybe (SizedList m r) -> Maybe (SizedList m r) -> Maybe (LinearConstraints k m r) -> Maybe (SizedList m r) -> Either LevMarError (SizedList m r, Info r, CovarMatrix m r) -- | Linear constraints consisting of a constraints matrix, kxn and -- a right hand constraints vector, kx1 where n is the -- number of parameters and k is the number of constraints. type LinearConstraints k n r = (Matrix k n r, SizedList k r) -- | Value to denote the absense of any linear constraints over the -- parameters of the model function. Use this instead of Nothing -- because the type parameter which contains the number of constraints -- can't be inferred. noLinearConstraints :: (Nat n) => Maybe (LinearConstraints Z n r) -- | A nxm matrix is a sized list of n sized lists of length -- m. type Matrix n m r = SizedList n (SizedList m r) -- | Minimization options data Options r Opts :: r -> r -> r -> r -> r -> Options r -- | Scale factor for initial mu. optScaleInitMu :: Options r -> r -- | Stopping thresholds for ||J^T e||_inf. optStopNormInfJacTe :: Options r -> r -- | Stopping thresholds for ||Dp||_2. optStopNorm2Dp :: Options r -> r -- | Stopping thresholds for ||e||_2. optStopNorm2E :: Options r -> r -- | Step used in the difference approximation to the Jacobian. If -- optDelta<0, the Jacobian is approximated with central -- differences which are more accurate (but slower!) compared to the -- forward differences employed by default. optDelta :: Options r -> r -- | Default minimization options defaultOpts :: (Fractional r) => Options r -- | Information regarding the minimization. data Info r Info :: r -> r -> r -> r -> r -> Integer -> StopReason -> Integer -> Integer -> Integer -> Info r -- | ||e||_2 at initial parameters. infNorm2initE :: Info r -> r -- | ||e||_2 at estimated parameters. infNorm2E :: Info r -> r -- | ||J^T e||_inf at estimated parameters. infNormInfJacTe :: Info r -> r -- | ||Dp||_2 at estimated parameters. infNorm2Dp :: Info r -> r -- | mu/max[J^T J]_ii ] at estimated parameters. infMuDivMax :: Info r -> r -- | Number of iterations. infNumIter :: Info r -> Integer -- | Reason for terminating. infStopReason :: Info r -> StopReason -- | Number of function evaluations. infNumFuncEvals :: Info r -> Integer -- | Number of jacobian evaluations. infNumJacobEvals :: Info r -> Integer -- | Number of linear systems solved, i.e. attempts for reducing error. infNumLinSysSolved :: Info r -> Integer -- | Reason for terminating. data StopReason -- | Stopped because of small gradient J^T e. SmallGradient :: StopReason -- | Stopped because of small Dp. SmallDp :: StopReason -- | Stopped because maximum iterations was reached. MaxIterations :: StopReason -- | Stopped because of singular matrix. Restart from current estimated -- parameters with increased optScaleInitMu. SingularMatrix :: StopReason -- | Stopped because no further error reduction is possible. Restart with -- increased optScaleInitMu. SmallestError :: StopReason -- | Stopped because of small ||e||_2. SmallNorm2E :: StopReason -- | Stopped because model function returned invalid values (i.e. NaN or -- Inf). This is a user error. InvalidValues :: StopReason -- | Covariance matrix corresponding to LS solution. type CovarMatrix n r = Matrix n n r data LevMarError -- | Generic error (not one of the others) LevMarError :: LevMarError -- | A call to a lapack subroutine failed in the underlying C levmar -- library. LapackError :: LevMarError -- | At least one lower bound exceeds the upper one. FailedBoxCheck :: LevMarError -- | A call to malloc failed in the underlying C levmar library. MemoryAllocationFailure :: LevMarError -- | The matrix of constraints cannot have more rows than columns. ConstraintMatrixRowsGtCols :: LevMarError -- | Constraints matrix is not of full row rank. ConstraintMatrixNotFullRowRank :: LevMarError -- | Cannot solve a problem with fewer measurements than unknowns. In case -- linear constraints are provided, this error is also returned when the -- number of measurements is smaller than the number of unknowns minus -- the number of equality constraints. TooFewMeasurements :: LevMarError -- | Type-level natural denoting zero data Z -- | Type-level natural denoting the Successor of another type-level -- natural. data S n -- | Class of all type-level naturals. class Nat n -- | A list which is indexed with a type-level natural that denotes the -- size of the list. data SizedList n a Nil :: SizedList Z a (:::) :: a -> SizedList n a -> SizedList (S n) a -- | A NFunction n a b is a function which takes n -- arguments of type a and returns a b. For example: -- NFunction (S (S (S Z))) a b ~ (a -> a -> a -> b) -- | A levmar variant that uses Automatic Differentiation to automatically -- compute the Jacobian. -- -- For additional documentation see the documentation of the levmar C -- library which this library is based on: -- http://www.ics.forth.gr/~lourakis/levmar/ module LevMar.AD -- | A functional relation describing measurements represented as a -- function from m parameters to n expected -- measurements. -- -- An example from Demo.hs: -- --
-- type N4 = S (S (S (S Z))) -- -- hatfldc :: Model N4 N4 Double -- hatfldc p0 p1 p2 p3 = p0 - 1.0 -- ::: p0 - sqrt p1 -- ::: p1 - sqrt p2 -- ::: p3 - 1.0 -- ::: Nil --type Model m n r = NFunction m r (SizedList n r) -- | The Levenberg-Marquardt algorithm is overloaded to work on -- Double and Float. class LevMarable r -- | The Levenberg-Marquardt algorithm that automatically computes the -- Jacobian using automatic differentiation of the model function. -- -- Warning: Don't apply levmar to Models that apply -- methods of the Eq and Ord classes to the parameters. -- These methods are undefined for ':~>'!!! levmar :: (Nat m, Nat n, Nat k, HasBasis r, (Basis r) ~ (), VectorSpace (Scalar r), LevMarable r) => (Model m n (r :~> r)) -> SizedList m r -> SizedList n r -> Integer -> Options r -> Maybe (SizedList m r) -> Maybe (SizedList m r) -> Maybe (LinearConstraints k m r) -> Maybe (SizedList m r) -> Either LevMarError (SizedList m r, Info r, CovarMatrix m r) -- | Linear constraints consisting of a constraints matrix, kxn and -- a right hand constraints vector, kx1 where n is the -- number of parameters and k is the number of constraints. type LinearConstraints k n r = (Matrix k n r, SizedList k r) -- | Value to denote the absense of any linear constraints over the -- parameters of the model function. Use this instead of Nothing -- because the type parameter which contains the number of constraints -- can't be inferred. noLinearConstraints :: (Nat n) => Maybe (LinearConstraints Z n r) -- | A nxm matrix is a sized list of n sized lists of length -- m. type Matrix n m r = SizedList n (SizedList m r) -- | Minimization options data Options r Opts :: r -> r -> r -> r -> r -> Options r -- | Scale factor for initial mu. optScaleInitMu :: Options r -> r -- | Stopping thresholds for ||J^T e||_inf. optStopNormInfJacTe :: Options r -> r -- | Stopping thresholds for ||Dp||_2. optStopNorm2Dp :: Options r -> r -- | Stopping thresholds for ||e||_2. optStopNorm2E :: Options r -> r -- | Step used in the difference approximation to the Jacobian. If -- optDelta<0, the Jacobian is approximated with central -- differences which are more accurate (but slower!) compared to the -- forward differences employed by default. optDelta :: Options r -> r -- | Default minimization options defaultOpts :: (Fractional r) => Options r -- | Information regarding the minimization. data Info r Info :: r -> r -> r -> r -> r -> Integer -> StopReason -> Integer -> Integer -> Integer -> Info r -- | ||e||_2 at initial parameters. infNorm2initE :: Info r -> r -- | ||e||_2 at estimated parameters. infNorm2E :: Info r -> r -- | ||J^T e||_inf at estimated parameters. infNormInfJacTe :: Info r -> r -- | ||Dp||_2 at estimated parameters. infNorm2Dp :: Info r -> r -- | mu/max[J^T J]_ii ] at estimated parameters. infMuDivMax :: Info r -> r -- | Number of iterations. infNumIter :: Info r -> Integer -- | Reason for terminating. infStopReason :: Info r -> StopReason -- | Number of function evaluations. infNumFuncEvals :: Info r -> Integer -- | Number of jacobian evaluations. infNumJacobEvals :: Info r -> Integer -- | Number of linear systems solved, i.e. attempts for reducing error. infNumLinSysSolved :: Info r -> Integer -- | Reason for terminating. data StopReason -- | Stopped because of small gradient J^T e. SmallGradient :: StopReason -- | Stopped because of small Dp. SmallDp :: StopReason -- | Stopped because maximum iterations was reached. MaxIterations :: StopReason -- | Stopped because of singular matrix. Restart from current estimated -- parameters with increased optScaleInitMu. SingularMatrix :: StopReason -- | Stopped because no further error reduction is possible. Restart with -- increased optScaleInitMu. SmallestError :: StopReason -- | Stopped because of small ||e||_2. SmallNorm2E :: StopReason -- | Stopped because model function returned invalid values (i.e. NaN or -- Inf). This is a user error. InvalidValues :: StopReason -- | Covariance matrix corresponding to LS solution. type CovarMatrix n r = Matrix n n r data LevMarError -- | Generic error (not one of the others) LevMarError :: LevMarError -- | A call to a lapack subroutine failed in the underlying C levmar -- library. LapackError :: LevMarError -- | At least one lower bound exceeds the upper one. FailedBoxCheck :: LevMarError -- | A call to malloc failed in the underlying C levmar library. MemoryAllocationFailure :: LevMarError -- | The matrix of constraints cannot have more rows than columns. ConstraintMatrixRowsGtCols :: LevMarError -- | Constraints matrix is not of full row rank. ConstraintMatrixNotFullRowRank :: LevMarError -- | Cannot solve a problem with fewer measurements than unknowns. In case -- linear constraints are provided, this error is also returned when the -- number of measurements is smaller than the number of unknowns minus -- the number of equality constraints. TooFewMeasurements :: LevMarError -- | Type-level natural denoting zero data Z -- | Type-level natural denoting the Successor of another type-level -- natural. data S n -- | Class of all type-level naturals. class Nat n -- | A list which is indexed with a type-level natural that denotes the -- size of the list. data SizedList n a Nil :: SizedList Z a (:::) :: a -> SizedList n a -> SizedList (S n) a -- | A NFunction n a b is a function which takes n -- arguments of type a and returns a b. For example: -- NFunction (S (S (S Z))) a b ~ (a -> a -> a -> b)