3

I am using a system called CLaSH. For those who are not familiar it is designed in a way that allows you to develop for FPGAs using Haskell.

I am trying to create an Unsigned value. 

Defined at: https://hackage.haskell.org/package/clash-prelude-0.10.11/docs/src/CLaSH-Sized-Internal-Unsigned.html#Unsigned

Something like: 

2 :: Unsigned 3

works. I want to be able to do something like:

x = 3

2::Unsigned x

But I get the error:

No instance for (KnownNat x1) arising from the literal `2'

 

Possible fix:

 add (KnownNat x1) to the context of

 an expression type signature: Unsigned x1

 In the expression: 2 :: Unsigned x

 In an equation for `it': it = 2 :: Unsigned x

I then tried "fromInteger#" defined in the same file. 

let y=fromInteger# x

which returns the type

y :: KnownNat n => Unsigned n

With that 'y' I can give it a size by adding an unsigned with a specified size. 

y + (2 :: Unsigned 3)

which gives a  5

it :: Unsigned 3

How do I get a something like 

2::Unsigned x

If I can't do this, why can't I?

EDIT: It is possible to do what I needed using template Haskell. See code below and link to CLaSH group explanation

https://groups.google.com/forum/#!topic/clash-language/uPjt8i0lF0M . 

What I wanted I could accomplish at compile time. Runtime would be impossible.

error_null_pointer
  • 457
  • 1
  • 6
  • 21

1 Answers1

4

If I understand you correctly, you want to be able to reference variables as type-level naturals in your type signatures. For this you have to declare x as a type (type or data) rather than a value. It is this distinction between values and types that separates Haskell from the older stock of dependently-typed languages, where you would be able to freely reference declarations in types without worrying about the differences between values and types. So, try making your code look something like this:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}

module Lib where

import Data.Proxy
import GHC.TypeLits

data Unsigned (a :: Nat)
type X = 2

main :: IO ()
main =
  print (Proxy :: Proxy (Unsigned X))

I fear that I do not know anything about Clash, however, so perhaps I do not have the whole picture.

hao
  • 10,138
  • 1
  • 35
  • 50
  • How would I define a type of data in a way that lets me use a value? The end goal is to get an unsigned value of size f(x) I.e. 5 :: Unsigned f(x) if I understand you answer there would be no way of doing that because types and values are different. – error_null_pointer Aug 15 '16 at 18:28
  • is `x` known at compiletime? types only exist at compiletime and then, when your program is run, are erased and gone and poof were never there all along – hao Aug 15 '16 at 18:29
  • It would not be known at compile time. The value f(x) would be determined during runtime. – error_null_pointer Aug 15 '16 at 18:36
  • I managed to redesign and restructure the code to know the values at run time. However I still have one value f(x) I'd like to compute. I can set the x to a type but I'd like to compute f(x) automatically instead of by hand. This is ensure that we can make changes in the source code quickly. – error_null_pointer Aug 15 '16 at 19:56
  • it is impossible, in general, to have types depend on runtime values – hao Aug 15 '16 at 22:18
  • I was able to do what I needed at compile time thanks to template Haskell. – error_null_pointer Aug 16 '16 at 19:17