loadOrder :: (ЭтоНесущественныеДеталиРеализации k) => Int -> SomeSing k

data SomeSing (kproxy :: KProxy k) where
    SomeSing :: Sing (a :: k) -> SomeSing ('KProxy :: KProxy k)

case order of SomeSing order' -> procOrder order'

procOrder :: Sing (order :: OrderDescription) -> Result

{-# LANGUAGE PolyKinds, DataKinds #-}
{-# LANGUAGE TypeFamilies, GADTs #-}

{-# LANGUAGE NPlusKPatterns #-}

{-# LANGUAGE TypeOperators #-}

import Data.Singletons
import Data.Singletons.Prelude

data Nat = Z | S Nat -- Nat это и тип и кайнд (тип типов)

integerToNat 0 = Z
integerToNat (n + 1) = S (integerToNat n)

-- Все что ниже генерируется автоматически
-- genSingletons [''Nat]
-- но приведено для образовательных целей

-- это синглетон для Nat
data instance Sing (n :: Nat) where
  SZ :: Sing Z
  SS :: Sing n -> Sing (S n)

-- механизм трансляции между значениями типа Nat и значениями синглетон-типа
instance SingKind ('KProxy :: KProxy Nat) where
  type DemoteRep ('KProxy :: KProxy Nat) = Nat

  fromSing SZ = Z
  fromSing (SS n) = S (fromSing n)
  
  toSing Z = SomeSing SZ
  toSing (S n) = case toSing n :: SomeSing ('KProxy :: KProxy Nat) of
    SomeSing k -> SomeSing (SS k)

-- конец автоматически генерируемого бойлерплейта

-- функция создает вложенные списки (если n > 0)
create :: Sing (n :: Nat) -> MyType n
create SZ = 0
create (SS x) = [create x]

-- разных типов в зависимости
-- от передаваемого ей значения.
type family MyType (a :: Nat)
type instance MyType Z = Int
type instance MyType (S x) = [MyType x]

-- функция сериализует в строку эти списки (разных типов)
-- тут от передаваемого значения зависит тип другого принимаемого значения
useValue :: Sing (n :: Nat) -> MyType n -> String
useValue SZ v = show v
useValue (SS x) v = "[" ++ (concat $ map (useValue x) v) ++ "]"

main = do
  ns <- getLine -- пользователь вводит число с клавиатуры
  let n = integerToNat . read $ ns -- парсим его
  -- создаем из этого числа синглетон, дальше внутри лямбды
  -- это число будет типом. 
  putStrLn $ withSomeSing n (\n -> useValue n (create n))

J>>А можно вернуть "просто ордер", как в моем примере по ссылке — но ты с ним ничего реального не сможешь сделать. Вернее, сможешь, но только после проверки необходимых свойств — и попытки вызвать код для ордера, у которого необходимые свойства не проверены, просто не скомпилируются.
S>Пока непонятно. Получается, мы не можем персисить ордер за пределы текущего процесса — а это очень плохо, т.к. типичные workflow ордеров катастрофически медленные. Требование держать всё в памяти — невыполнимо.

Посмотри на мой код

Автор: jazzer
Дата: 10.02.15

по ссылке все же (я понимаю, что лень, но все-таки). Там есть свойства, которые сидят прямо в ордере, и замечательно "персистятся".
Так что сделал check_fraud, записал результат order.fraud_checked=true, order.fraud_check_result=true, заперсистил. У тебя уже новый тип, как после долгой проверки, так и после загрузки "заперсисченного" ордера из БД, непосредственно из order.fraud_check_result.

public void Order increase_amount(Order order, Money newAmount)
{
  Contracts.Assert(order, (o)=> !o.HasRisk); // выбросим исключение!
  Contracts.Assert(order, (o)=> !o.Shipped); // выбросим исключение!

  Contracts.Assert(order, (o)=> newAmount <= 1.20 * o.CurrentAmount) // выбросим исключение!

  return order.Clone().SetAmount(newAmount);
}

public void Order<Risk.None, Shipped.None> increase_amount(Order<Risk.None, Shipped.None> order, Money newAmount)
{
  Contracts.Assert(order, (o)=> newAmount <= 1.20 * o.CurrentAmount) // выбросим исключение!
  return order.Clone().SetAmount(newAmount);
}

public void Order try_increase_amount(Order order, Money newAmount)
{
  var o = checkNoRisk(order); // выбросим исключение, если есть риск, вернём Order<Risk.None, S> иначе
  var o2 = checkNotShipped(o); // выбросим исключение, если зашиплен, вернём Order<Risk.None, Shipped.None> иначе

  return increase_amount(order // не компилируется
                         o // не компилируется
                         o2, newAmount); // ура, компилируется!!!
}

S>public void Order increase_amount(Order order, Money newAmount)
S>{
S>  Contracts.Assert(order, (o)=> !o.HasRisk); // выбросим исключение!
S>  Contracts.Assert(order, (o)=> !o.Shipped); // выбросим исключение!
S>  Contracts.Assert(order, (o)=> newAmount <= 1.20 * o.CurrentAmount) // выбросим исключение!
S>  return order.Clone().SetAmount(newAmount);
S>}
S>

EP>Нарушение предусловия это баг в программе, программа находится в том состоянии в котором не должна была по логике вещей, и как она туда попала неизвестно, лучше всего пристрелить такую программу как взбесившуюся собаку. Почитай наконец что такое precondition.
EP>Предусловия можно проверять, и как-то энфорсить, но отнюдь не обязательно. Например assert'ы энфорсящие предусловия часто используют только в отладочных режимах.
EP>Система типов позволяет энфорсить некоторые предусловия в compile-time, но не все. Я даже больше скажу, далеко не все предусловия можно проверить в runtime — попытка такой проверки попросту может поломать инварианты, и сделать невозможным достижение постусловий.

...
S>  var o = checkNoRisk(order); // выбросим исключение, если есть риск, вернём Order<Risk.None, S> иначе
S>  var o2 = checkNotShipped(o); // выбросим исключение, если зашиплен, вернём Order<Risk.None, Shipped.None> иначе
S>...

EP>Если же для запуска функции нет необходимости делать проверки, change_amount сама всё что нужно проверяет внутри, и более того её запуск с невыполненными условиями не является ошибкой, а вполне штатным режимом — то пытаться переписать все эти внутренние проверки на типы, не вижу смысла, это никак не отразится на местах вызова этой функции.

Order = load_order(Id),
UpdatedOrder = process_order(Order).  
  %% внутри process_order «это действительно не имеет смысла» ©

....

%% в другом месте

Order = load_order(Id),
UpdatedOrder = increase_order_amount(Order, Amount).
  %% внутри increase_order_amount «это действительно не имеет смысла» ©


%% в третьем месте

Order = load_order(Id),
UpdatedOrder = archive_order(Order).
  %% внутри archive_order «это действительно не имеет смысла» ©

%% и т.п.

M>Я про это тоже говорил. Ты придумал себе какие-то предусловия и активно пытаешься это энфорсить. В моем случае условия никуда не исчезли — это все те же условия. Только ВНЕЗАПНО для них «не имеет смысла»

EP>Состояние ранее являвшееся ошибкой, стало вполне штатным режимом работы, и это повлияло на возможные варианты реализации этого в коде. И что тебя удивляет?