Any plan to upload to Hackage?

[pe200012]

Hi,

I found your interesting library and wanted to use it in my personal project, but it seems like typed-fsm is nowhere on hackage. Although I could add it as git dependency in stack.yml, being available on hackage may help increase its accessibility.

[sdzx-1]

This library is still changing rapidly, and I hope to add singletons. However, dependent-sum-template and singletons do not seem to be compatible at the moment. So in the long run I will publish this library to hackage, but probably not in the short term. link

[sdzx-1]

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module MyLib where

import Data.GADT.Compare (GCompare (..), GEq (..), GOrdering (..))
import Data.GADT.Compare.TH (
  DeriveGCompare (deriveGCompare),
  DeriveGEQ (deriveGEq),
 )
import Data.Kind
import Data.Singletons.Base.TH
import Data.Singletons.TH.Options
import Data.Singletons.TH.Options (defaultOptions)
import Data.Type.Equality (TestEquality (testEquality))
import Language.Haskell.TH (Q)
import Language.Haskell.TH.Syntax (runQ)
import Unsafe.Coerce (unsafeCoerce)

$( singletons
    [d|
      data N = Z | S N deriving (Show, Eq, Ord)
      |]
 )

sOrdToGCompare :: forall n (a :: n) (b :: n). (SOrd n) => Sing a -> Sing b -> GOrdering a b
sOrdToGCompare a b = case sCompare a b of
  SEQ -> unsafeCoerce GEQ
  SLT -> GLT
  SGT -> GGT

instance GEq SN where
  geq = testEquality

instance GCompare SN where
  gcompare a b = sOrdToGCompare a b

$( singletons
    [d|
      data N = Z | S N deriving (Show, Eq, Ord)
      |]
 )

deriving (Show, Eq, Ord) will produce SEq, SOrd.

They are equivalent to GEq, GCompare. Therefore, using the function testEquality, sOrdToGCompare can instantne GEq, GCompare.

ATM example:

$( singletons
    [d|
      data N = Z | S N
        deriving (Show, Eq, Ord)

      data ATMSt
        = Ready
        | CardInserted N
        | CheckPin N
        | Session
        | Exit
        deriving (Show, Eq, Ord)
      |]
 )

satmToatm :: SATMSt s -> ATMSt
satmToatm = fromSing

instance GEq SN where
  geq = testEquality

instance GEq SATMSt where
  geq = testEquality

instance GCompare SN where
  gcompare = sOrdToGCompare

instance GCompare SATMSt where
  gcompare = sOrdToGCompare

motion example:

$( singletons
    [d|
      data Motion
        = Idle
        | Over
        | Hover
        | Exit
        deriving (Show, Eq, Ord)
      |]
 )

instance GEq SMotion where
  geq = testEquality

instance GCompare SMotion where
  gcompare = sOrdToGCompare

[pe200012]

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module MyLib where

import Data.GADT.Compare (GCompare (..), GEq (..), GOrdering (..))
import Data.GADT.Compare.TH (
  DeriveGCompare (deriveGCompare),
  DeriveGEQ (deriveGEq),
 )
import Data.Kind
import Data.Singletons.Base.TH
import Data.Singletons.TH.Options
import Data.Singletons.TH.Options (defaultOptions)
import Data.Type.Equality (TestEquality (testEquality))
import Language.Haskell.TH (Q)
import Language.Haskell.TH.Syntax (runQ)
import Unsafe.Coerce (unsafeCoerce)

$( singletons
    [d|
      data N = Z | S N deriving (Show, Eq, Ord)
      |]
 )

sOrdToGCompare :: forall n (a :: n) (b :: n). (SOrd n) => Sing a -> Sing b -> GOrdering a b
sOrdToGCompare a b = case sCompare a b of
  SEQ -> unsafeCoerce GEQ
  SLT -> GLT
  SGT -> GGT

instance GEq SN where
  geq = testEquality

instance GCompare SN where
  gcompare a b = sOrdToGCompare a b

$( singletons
    [d|
      data N = Z | S N deriving (Show, Eq, Ord)
      |]
 )

deriving (Show, Eq, Ord) will produce SEq, SOrd.

They are equivalent to GEq, GCompare. Therefore, using the function testEquality, sOrdToGCompare can instantne GEq, GCompare.

ATM example:

$( singletons
    [d|
      data N = Z | S N
        deriving (Show, Eq, Ord)

      data ATMSt
        = Ready
        | CardInserted N
        | CheckPin N
        | Session
        | Exit
        deriving (Show, Eq, Ord)
      |]
 )

satmToatm :: SATMSt s -> ATMSt
satmToatm = fromSing

instance GEq SN where
  geq = testEquality

instance GEq SATMSt where
  geq = testEquality

instance GCompare SN where
  gcompare = sOrdToGCompare

instance GCompare SATMSt where
  gcompare = sOrdToGCompare

motion example:

$( singletons
    [d|
      data Motion
        = Idle
        | Over
        | Hover
        | Exit
        deriving (Show, Eq, Ord)
      |]
 )

instance GEq SMotion where
  geq = testEquality

instance GCompare SMotion where
  gcompare = sOrdToGCompare

So, we can now eliminate the dependency on dependent-sum-template...?

[sdzx-1]

Yes.

[sdzx-1]

https://hackage.haskell.org/package/typed-fsm

[pe200012]

Good to see that! I'll leave this issue for you to close ;)