Skip to content

Instantly share code, notes, and snippets.

@cdepillabout
Last active June 11, 2021 11:53
Show Gist options
  • Save cdepillabout/91f6a36f3451e1026bdd01e83c3ba5fb to your computer and use it in GitHub Desktop.
Save cdepillabout/91f6a36f3451e1026bdd01e83c3ba5fb to your computer and use it in GitHub Desktop.
This file shows how similar existential types are vs. sigma types (dependent pairs).
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeInType #-}
module VectStuff20 where
import Data.Constraint (Dict(Dict))
import Data.Kind (Type)
import Data.Proxy (Proxy(Proxy))
import GHC.Natural (Natural)
import Data.Singletons
import Data.Singletons.Prelude
import Data.Singletons.Decide
((:~:)(Refl), Decision(Disproved, Proved), Refuted, (%~))
import Data.Singletons.Sigma (Sigma((:&:)))
import Data.Singletons.TypeLits (KnownNat, Nat, Sing(SNat))
import Unsafe.Coerce (unsafeCoerce)
data Vect :: Type -> Nat -> Type where
VNil :: Vect a 0
VCons :: a -> Vect a n -> Vect a (n + 1)
deriving instance Show a => Show (Vect a n)
plusMinus1Law :: forall (n :: Nat) m. n :~: ((n - m) + m)
plusMinus1Law = unsafeCoerce Refl
data Magic = Magic Natural
natToSing :: forall (n :: Nat). Natural -> Sing n
natToSing = unsafeCoerce Magic
gtZeroMinusNat :: Sing n -> Refuted (n :~: 0) -> Sing (n - 1)
gtZeroMinusNat sNat _ = natToSing (fromSing sNat - 1)
replicateVect :: forall n a. Sing n -> a -> Vect a n
replicateVect sNatN a =
case sNatN %~ (sing @_ @0) of
Proved Refl -> VNil
Disproved f ->
case plusMinus1Law @n @1 of
Refl ->
case gtZeroMinusNat sNatN f of
snatNMinus1 -> VCons a $ replicateVect snatNMinus1 a
testReplicateVect :: Vect String 3
testReplicateVect = replicateVect (sing @_ @3) "hello"
data SomeVect :: Type -> Type where
SomeVect :: forall a n. KnownNat n => Vect a n -> SomeVect a
deriving instance Show a => Show (SomeVect a)
replicateExistentialVect :: forall n a. Natural -> a -> SomeVect a
replicateExistentialVect nat a =
case toSing nat of
SomeSing sNat ->
case sNat of
SNat -> SomeVect $ replicateVect sNat a
testReplicateExistentialVect :: IO ()
testReplicateExistentialVect =
case replicateExistentialVect 3 "hello" of
SomeVect vect -> print vect
replicateSigmaVect :: forall n a. Natural -> a -> Sigma Nat (TyCon (Vect a))
replicateSigmaVect nat a =
case toSing nat of
SomeSing sNat -> sNat :&: replicateVect sNat a
testReplicateSigmaVect :: IO ()
testReplicateSigmaVect =
case replicateSigmaVect 3 "hello" of
_ :&: vect -> print vect
existentialToSigma :: forall a. SomeVect a -> Sigma Nat (TyCon (Vect a))
existentialToSigma (SomeVect (vect :: Vect a n)) = sing :&: vect
sigmaToExistential :: Sigma Nat (TyCon (Vect a)) -> SomeVect a
sigmaToExistential (SNat :&: vect) = SomeVect vect
-- | Generalized existential type.
data Ex :: (k -> Type) -> Type where
Ex :: a i -> Ex a
replicateGenExistentialVect :: forall n a. Natural -> a -> Ex (Vect a)
replicateGenExistentialVect nat a =
case toSing nat of
SomeSing sNat -> Ex $ replicateVect sNat a
testReplicateGenExistentialVect :: IO ()
testReplicateGenExistentialVect =
case replicateGenExistentialVect 3 "hello" of
Ex vect -> print vect
@cdepillabout
Copy link
Author

This can be loaded into ghci with the following command:

$ stack --resolver nightly-2018-03-18 ghci --package singletons --package constraints

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment