• solrize@lemmy.ml
    link
    fedilink
    arrow-up
    10
    ·
    edit-2
    1 day ago

    This is probably an ok use for a GADT. Something like:

    {-# LANGUAGE DataKinds      #-}
    {-# LANGUAGE GADTs          #-}
    {-# LANGUAGE KindSignatures #-}
    
    data Bap = Baptized | Unbaptized
    
    data Person :: Bap -> * where
       Baptize :: Person Unbaptized -> Person Baptized
       NewPerson :: Person Unbaptized
    
    conditionalBaptize :: Person a -> Person Baptized
    conditionalBaptize p =
        case p of NewPerson -> Baptize p
                  Baptize _ -> p
    
    main = return ()