On Mar 15, 2014, at 4:48 PM, Henning Thielemann wrote:
What is the meaning of KnownNat?
It is a Nat whose value is known at runtime. I'll confess to suggesting the
nameā¦ I think I was hoping there would be more debate and a better idea at the
time, but it just stuck.
I see that there is no
To answer your second question using GADT-style vectors:
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators#-}
{-# LANGUAGE ScopedTypeVariables #-}
module WithVector where
import Data.Maybe
import Data.Proxy
Am 15.03.2014 19:17, schrieb Erik Hesselink:
I think most of the singletons stuff has been moved to the
'singletons' package [0].
Yes, that's it. It means that all Nat related functionality in
'singletons' can be implemented using GHC.TypeLits - interesting.
Using the library I succeeded