Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
A length-indexed list where the length is ad-hoc polymorphic (using singletons)
let
nixpkgsTarball = builtins.fetchTarball {
name = "nixos-unstable-2018-11-09";
url = https://github.com/nixos/nixpkgs/archive/1c49226176d248129c795f4a654cfa9d434889ae.tar.gz;
sha256 = "0v8vp38lh6hqazfwxhngr5j96m4cmnk1006kh5shx0ifsphdip62";
};
nixpkgs = import nixpkgsTarball { };
in
with nixpkgs;
let
ghc862 =
haskell.packages.ghc862.override {
overrides = self: super: {
singletons = haskell.lib.overrideCabal super.singletons (drv: {
version = "2.5";
sha256 = "0bk1ad4lk4vc5hw2j4r4nzs655k43v21d2s66hjvp679zxkvzz44";
});
th-desugar = self.callHackage "th-desugar" "1.9" {};
};
};
ghcWithPkgs =
ghc862.ghcWithPackages (pkgs: with pkgs; [ singletons ]);
in
pkgs.mkShell {
buildInputs = [ ghcWithPkgs ];
}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
import Data.Coerce
import Data.Kind (Type)
import Data.Singletons
import Data.Singletons.Prelude
import Data.Singletons.TH
import Data.Singletons.TypeLits
import Numeric.Natural (Natural)
import Unsafe.Coerce
-- Define a Peano datatype and some helper functions.
$(singletons [d|
data Peano = Z | S Peano deriving (Eq, Ord, Show)
addPeano :: Peano -> Peano -> Peano
addPeano Z a = a
addPeano (S a) b = S (addPeano a b)
subtractPeano :: Peano -> Peano -> Peano
subtractPeano Z _ = Z
subtractPeano a Z = a
subtractPeano (S a) (S b) = subtractPeano a b
multPeano :: Peano -> Peano -> Peano
multPeano Z _ = Z
multPeano (S a) b = addPeano (multPeano a b) b
n0 :: Peano
n0 = Z
n1 :: Peano
n1 = S n0
n2 :: Peano
n2 = S n1
n3 :: Peano
n3 = S n2
n4 :: Peano
n4 = S n3
n5 :: Peano
n5 = S n4
n6 :: Peano
n6 = S n5
n7 :: Peano
n7 = S n6
n8 :: Peano
n8 = S n7
n9 :: Peano
n9 = S n8
n10 :: Peano
n10 = S n9
instance Num Peano where
(+) = addPeano
(-) = subtractPeano
(*) = multPeano
abs = id
signum Z = Z
signum (S _) = S Z
fromInteger n = if n == 0 then Z else S (fromInteger (n - 1))
|])
-- | Create a kind-class for defining the 'ToNat' type family. This gives us a way
-- to convert an @(n :: k)@ to a Nat.
--
-- Below, we create an instance of it for 'Nat' and 'Peano'.
class (SDecide k, SNum k, PNum k) => PToNat k where
type family ToNat (n :: k) :: Nat
instance PToNat Nat where
type ToNat n = n
instance PToNat Peano where
type ToNat 'Z = 0
type ToNat ('S n) = 1 + ToNat n
-- | This is quite a complicated kind-class. It declares the 'VecIdxZero' and
-- 'VecIdxSucc' type families. These let you figure out what types to use for
-- the \"zero\" and \"succ\" elements for a 'Vec' parameterized by the kind
-- @k@.
--
-- There are instances of this for 'Nat' and 'Peano'.
class
( VecIdxZero k ~ FromInteger 0
, ToNat (VecIdxZero k) ~ 0
, PToNat k
, forall (n :: k). (FromInteger 0 + n) ~ n
) => VecIdx k where
type family VecIdxZero k :: k
type family VecIdxSucc k :: k ~> k
instance VecIdx Nat where
type VecIdxZero Nat = 0
-- This is the defunctionalization version of @(+ 1)@.
type VecIdxSucc Nat = ((+@#@$$) 1)
instance VecIdx Peano where
type VecIdxZero Peano = 'Z
-- This is the defunctionalization version of @'S@.
type VecIdxSucc Peano = TyCon 'S
-- A length-indexed list where the index is polymorphic over the 'VecIdx'
-- kind-class.
data Vec (k :: Type) (n :: k) :: Type -> Type where
EmptyVec :: Vec k (VecIdxZero k) a
ConsVec :: a -> Vec k n a -> Vec k (VecIdxSucc k @@ n) a
deriving instance Show a => Show (Vec k n a)
-- Singleton function for 'Vec' indexed by either 'Peano' or 'Nat'.
singletonVecPeano' :: a -> Vec Peano N1 a
singletonVecPeano' a = ConsVec a EmptyVec
singletonVecNat' :: a -> Vec Nat 1 a
singletonVecNat' a = ConsVec a EmptyVec
-- | Super-unsafe axiom that could prove anything. Use with care.
axiom :: forall a b. a :~: b
axiom = unsafeCoerce (Refl :: Int :~: Int)
-- | This is a proof. It can be read as follows:
--
-- Given that @n@ is not zero, then @Succ (n - 1) == n@.
proofSubtract1Succ
:: forall k (n :: k)
. Refuted (n :~: VecIdxZero k)
-> ((VecIdxSucc k) @@ (n - FromInteger 1)) :~: n
proofSubtract1Succ _ = axiom
-- These are some simple proofs that say adding 0 to any 'PNum' is the same as
-- doing nothing.
zeroPlusLL :: forall k (n :: k). (PNum k) => (FromInteger 0 + n) :~: n
zeroPlusLL = axiom
zeroPlusLR :: forall k (n :: k). (PNum k) => (n + FromInteger 0) :~: n
zeroPlusLR = axiom
-- | This says that if we know that @Succ n'@ is @n@, then we know that @Succ
-- (n' + m)@ is the same as @n + m@.
succPlus1 :: forall k n n' m. (n ~ (VecIdxSucc k @@ n')) => (VecIdxSucc k @@ (n' + m)) :~: (n + m)
succPlus1 = axiom
-- | This is a proof that addition commutes.
additionCommute :: forall n m. (n + m) :~: (m + n)
additionCommute = axiom
-- | Just like 'replicate' for lists.
replicateVec :: forall k n a. VecIdx k => Sing n -> a -> Vec k n a
replicateVec sn a =
case sFromInteger (sing @0) of
zeron ->
case sn %~ zeron of
Proved Refl -> EmptyVec
Disproved notZeroProof ->
case sFromInteger (sing @1) of
(onen :: Sing (FromInteger 1 :: k)) ->
case proofSubtract1Succ notZeroProof of
Refl -> a `ConsVec` replicateVec (sn %- onen) a
-- | Append two vectors.
appendVec :: forall k n m a. VecIdx k => Vec k n a -> Vec k m a -> Vec k (n + m) a
appendVec EmptyVec vec =
case zeroPlusLL @k @m of
Refl -> vec
appendVec vec EmptyVec =
case zeroPlusLR @k @n of
Refl -> vec
appendVec (ConsVec a (vecA :: Vec k n' a)) vecB =
case succPlus1 @k @n @n' @m of
Refl -> ConsVec a (appendVec vecA vecB)
-- | Zero-cost coercion from one vector type to another.
--
-- In order for this to work, @'ToNat' n@ has to be the same as @'ToNat' m@.
coerceVec
:: forall (k :: Type) (j :: Type) (n :: k) (m :: j) (a :: Type)
. ( VecIdx k
, VecIdx j
, ToNat n ~ ToNat m
)
=> Vec k n a
-> Vec j m a
coerceVec = unsafeCoerce
-- | Test that coercion actually works.
testCoerce :: forall (a :: Type). Vec Peano N5 a -> Vec Nat 5 a
testCoerce = coerceVec
-- | A vector that is polymorphic over the index kind. We know it is length 3.
testVec1 :: (SingI (FromInteger 3 :: k), VecIdx k) => Vec k (FromInteger 3) String
testVec1 = replicateVec sing "foo"
-- | A vector that is polymorphic over the index kind. We know it is length 4.
testVec2 :: (SingI (FromInteger 4 :: k), VecIdx k) => Vec k (FromInteger 4) String
testVec2 = replicateVec sing "bar"
-- | Test appending 'testVec1' and 'testVec2' together.
testAppVec :: Vec Peano N7 String
testAppVec = appendVec testVec1 testVec2
-- | Show how we can polymorphically append one element to a vec.
test
:: forall k n
. (VecIdx k, SingI (FromInteger 1 :: k))
=> Vec k n String
-> Vec k (n + FromInteger 1) String
test =
case additionCommute @(FromInteger 1) @n of
Refl ->
appendVec
(replicateVec
(sing @(FromInteger 1) :: Sing (FromInteger 1 :: k))
"hello"
)
@cdepillabout
Copy link
Author

cdepillabout commented Nov 11, 2018

This can be run in ghci like the following:

$ nix-shell my-ghc-8.6.2.nix --command 'ghci polymorphic-length-index.hs'
> testAppVec
ConsVec "foo" (ConsVec "foo" (ConsVec "foo" (ConsVec "bar" (ConsVec "bar" (ConsVec "bar" (ConsVec "bar" EmptyVec))))))

Loading

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