Linear Types and Dependent Types Outlook

40.1 Linear Types (GHC 9.0+)

Linear types enable safe resource management (files, mutable arrays freed exactly once) and in-place updates with a pure API. See the linear-base library.

{-# LANGUAGE LinearTypes #-}
-- a %1 -> b : the argument must be used exactly once
swapL :: (a, b) %1 -> (b, a)
swapL (x, y) = (y, x)

-- dup :: a %1 -> (a, a)    -- rejected: uses x twice
-- dup x = (x, x)

40.2 Toward Dependent Types

GHC is gradually gaining dependent-type features: TypeAbstractions, RequiredTypeArguments (GHC 9.10: visible forall a ->), and ongoing Dependent Haskell proposals.

Liquid Haskell adds refinement types checked by an SMT solver:

Related languages: Agda, Idris 2, Lean 4 (full dependent types), and PureScript, Elm, OCaml (functional cousins).

{-@ safeDiv :: Int -> {v:Int | v /= 0} -> Int @-}
safeDiv :: Int -> Int -> Int
safeDiv x y = x `div` y